[isabelle-dev] Checked "assume" command

Lawrence Paulson lp15 at cam.ac.uk
Wed Sep 5 14:54:19 CEST 2012

Simply fixing too many or too few variables. 

On 5 Sep 2012, at 13:52, Lars Noschinski <noschinl at in.tum.de> wrote:

>> 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

More information about the isabelle-dev mailing list