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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
