[isabelle] Schematic goal


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.


The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

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