Re: [isabelle] Schematic goal

Hello Michael,

since Isabelle2009-2, goal statements that involve schematic variables must be marked explicitly: Use schematic_lemma instead of lemma, schematic_theorem instead of theorem, etc. See also the NEWS file for this change.

Also note that you only need schematic type variables if you want to instantiate the type only during the proof and are too lazy to write this type down in full in the goal statement. If you want your lemma to be polymorphic, just omit the question mark and use an ordinary type variable. Existential type quantification is not possible in HOL anyway.

"EX (x::'a). ..."

Hope this helps,

Michael Chan schrieb:

I have a quick question about schematic goal statements in 2009-2. Are they allowed? I believe 2009-1 allows them, e.g., "EX (x::?'a)...". Now in 2009-2, I keep getting an error saying "Illegal schematic goal statement".

Any pointer will be appreciated. Thanks.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.