Re: [isabelle] Schematic goal
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
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
Any pointer will be appreciated. Thanks.
This archive was generated by a fusion of
Pipermail (Mailman edition) and