Email Gateway (Aug 22 2022 at 10:38): Email Gateway (Aug 22 2022 at 10:38):From: Buday Gergely <gbuday@karolyrobert.hu>
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.
Email Gateway (Aug 22 2022 at 10:38):From: Lars Hupel <hupel@in.tum.de>
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
Email Gateway (Aug 22 2022 at 10:38):From: Buday Gergely <gbuday@karolyrobert.hu>
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.
Email Gateway (Aug 22 2022 at 10:38):From: Lars Hupel <hupel@in.tum.de>
To typeset what the system responds to Isar language elements, as in the Output panel.
Sorry, but that is unclear to me. Do you mean the current goal state?
Email Gateway (Aug 22 2022 at 10:39):From: Buday Gergely <gbuday@karolyrobert.hu>
Yes, the current goal state.
Last updated: Apr 24 2024 at 20:16 UTC