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

Makarius wrote:
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.


Well, this is all very well, but I have dozens of emails showing that I tried to understand what these antiquotations do and why I should use them. When I failed to achieve any such understanding, I tried using them anyway, because you and others in Munich were so adamant that I should, saying that using the alternative calls would lead to errors.

The result of this was that introducing antiquotations into my code _caused_ errors, which were fixed when I reverted to not using them.



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