Re: [isabelle] Incompatibilities between releases (Re: Syntax for theory definitions)



On Thu, 9 Oct 2008, Jeremy Dawson wrote:

> Does this mean that all the functions involving an implicit context will 
> disappear? eg, Simp_tac, simpset, etc ?  My code is full of these.

Simp_tac and simpset: unit -> simpset are indeed legacy features, too, 
although not explicitly marked as such.  When embedding ML into Isar proof 
text, say via the method called "tactic", you can refer to the simpset 
from the context via the @{simpset} antiquotation.


	Makarius





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