712 defined on the logical level of Isabelle. By this we mean definitions, |
712 defined on the logical level of Isabelle. By this we mean definitions, |
713 theorems, terms and so on. This kind of reference is realised in Isabelle |
713 theorems, terms and so on. This kind of reference is realised in Isabelle |
714 with ML-antiquotations, often just called antiquotations.\footnote{There are |
714 with ML-antiquotations, often just called antiquotations.\footnote{There are |
715 two kinds of antiquotations in Isabelle, which have very different purposes |
715 two kinds of antiquotations in Isabelle, which have very different purposes |
716 and infrastructures. The first kind, described in this section, are |
716 and infrastructures. The first kind, described in this section, are |
717 \emph{ML-antiquotations}. They are used to refer to entities (like terms, |
717 \emph{\index*{ML-antiquotations}}. They are used to refer to entities (like terms, |
718 types etc) from Isabelle's logic layer inside ML-code. The other kind of |
718 types etc) from Isabelle's logic layer inside ML-code. The other kind of |
719 antiquotations are \emph{document} antiquotations. They are used only in the |
719 antiquotations are \emph{document}\index{document antiquotationa} antiquotations. |
|
720 They are used only in the |
720 text parts of Isabelle and their purpose is to print logical entities inside |
721 text parts of Isabelle and their purpose is to print logical entities inside |
721 \LaTeX-documents. Document antiquotations are part of the user level and |
722 \LaTeX-documents. Document antiquotations are part of the user level and |
722 therefore we are not interested in them in this Tutorial, except in Appendix |
723 therefore we are not interested in them in this Tutorial, except in Appendix |
723 \ref{rec:docantiquotations} where we show how to implement your own document |
724 \ref{rec:docantiquotations} where we show how to implement your own document |
724 antiquotations.} For example, one can print out the name of the current |
725 antiquotations.} For example, one can print out the name of the current |