[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. 
Larry

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