Re: [isabelle] @{context}



Lars Hupel wrote:

> > This is probably the most common antiquotation in interactive exper-
> > imentation with ML inside Isar.
> 
> this paragraph is important. @{context} is an ML antiquotation; that is, it can
> only be used in ML snippets (e.g. when using the "ML" or "ML_file" commands).

I see.

> > My aim is to look at the context between Isar proof elements.
> 
> What exactly do you mean with "look at"? A proof context contains a lot of
> information, some visible, some invisible, and just printing out the context
> would contain way to much information. Are you interested in fixed variables?
> Facts?

To typeset what the system responds to Isar language elements, as in the Output panel.

- Gergely




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