Email Gateway (Aug 22 2022 at 18:16): Email Gateway (Aug 22 2022 at 18:16):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi,
In one of the Isabelle source files the following appears:
\<^const_name>\<open>Trueprop\<close>
All I can find in the documentation is that \<open> and \<close> are
regular symbols and that \<^const_name> is a control symbol.
But none of them are listed in the Predefined Isabelle symbols in the
Appendix of the Isar reference manual.
What do all these mean? And How can one run such a file from isabelle
console?
Cheers,
Jeremy
Email Gateway (Aug 22 2022 at 18:16):From: Dominique Unruh <unruh@ut.ee>
Hi,
this is the same as @{const_name ‹True›}. In jEdit/PIDE, it will render
more prettily as const_name‹True›.
This is a (new?) mechanism for writing antiquotations with a single (or no)
argument.
You find a description in isar-ref (2018 version), Section 4.2.
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 18:16):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Dominique,
thanks for your help, much appreciated
Cheers,
Jeremy
Email Gateway (Aug 22 2022 at 18:17):From: Makarius <makarius@sketis.net>
Inside a use_thy for the theory that includes the ML/ML_file commands.
Makarius
Last updated: Apr 26 2024 at 16:20 UTC