Re: [isabelle] Schematic goal

>From the NEWS:

* Schematic theorem statements need to be explicitly markup as such,
via commands 'schematic_lemma', 'schematic_theorem',
'schematic_corollary'.  Thus the relevance of the proof is made
syntactically clear, which impacts performance in a parallel or
asynchronous interactive environment.  Minor INCOMPATIBILITY.

I was caught unawares by that as well recently.


Michael Chan schrieb:
> Hello,
> 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.
> Michael

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