Re: [isabelle] antiquotations

Makarius wrote:

In relation to advocating the use of antiquotations, you said:
It is determined from the context :-)

Pointing your finger at a particular position in Isar source text, you determine a certain context once and for all. Any embedded ML code at that point will keep this as a first-class value (of type Proof.context) for later use at run-time; provided proper antiquotations are used. So this is just the well-known static closure principle applied to Isabelle/Isar + embedded ML.

In contrast, low-level access to global references buys you dynamic scoping in the best case, and erratic non-determinism in the worst case. This is why thm"foo", thms"foo", the_context() are all bad.


(this was in relation to advocating the use of antiquotations)

But now I find that using @{theory} instead of the_context () produces an error

     "Stale theory encountered:\n{ProtoPure, Pur (etc)

When I change this back to the_context () the error goes away.

What is a stale theory, and why does @{theory} produce a stale theory?

Jeremy Dawson

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