[isabelle-dev] Checked "assume" command
noschinl at in.tum.de
Wed Sep 5 14:52:53 CEST 2012
On 05.09.2012 14:48, Lawrence Paulson wrote:
> Something of this general sort would certainly be useful. Having the wrong assumption is the most insidious of errors. The only similar one is misusing "fix". It would be great to be told when your context is wrong.
Which scenario do you have in mind with fix? The case where a too
general type is chosen, because the first mention of the fixed variable
also type-checks for a more general type?
More information about the isabelle-dev