Re: [isabelle] @{context}



Hi Gergely,

> 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 tried
> 
>     ML_file "$ISABELLE_HOME/src/Doc/antiquote_setup.ML"
> 
> but that did not work either. Is this still a valid antiquotation? The Isabelle/Isar Reference Manual does not list it.

I'll let Makarius comment here, but I'm pretty sure you're not supposed
to include ML files from somewhere in $ISABELLE_HOME unless you know
what you're doing.

> 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?

Cheers
Lars




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