[isabelle-dev] Checked "assume" command

[Lars Noschinski]

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?

   -- Lars