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