[isabelle] @{context}



Hi,

on page 49 the Implementation manual says:

--

@{context} refers to the context at compile-time - as abstract value. In-
dependently of (local) theory or proof mode, this always produces a
meaningful result.

This is probably the most common antiquotation in interactive exper-
imentation with ML inside Isar.

--

It does not work, the system says

   Undefined document antiquotation: "context"

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.

My aim is to look at the context between Isar proof elements.

- Gergely



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