equal
deleted
inserted
replaced
90 standard Isabelle fonts provide glyphs to render important control |
90 standard Isabelle fonts provide glyphs to render important control |
91 symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>". |
91 symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>". |
92 |
92 |
93 * Antiquotation @{theory_text} prints uninterpreted theory source text |
93 * Antiquotation @{theory_text} prints uninterpreted theory source text |
94 (outer syntax with command keywords etc.). This may be used in the short |
94 (outer syntax with command keywords etc.). This may be used in the short |
95 form \<^theory_text>\<open>...\<close>. |
95 form \<^theory_text>\<open>...\<close>. @{theory_text [display]} supports option "indent". |
|
96 |
|
97 * @{verbatim [display]} supports option "indent". |
96 |
98 |
97 * Antiquotation @{doc ENTRY} provides a reference to the given |
99 * Antiquotation @{doc ENTRY} provides a reference to the given |
98 documentation, with a hyperlink in the Prover IDE. |
100 documentation, with a hyperlink in the Prover IDE. |
99 |
101 |
100 * Antiquotations @{command}, @{method}, @{attribute} print checked |
102 * Antiquotations @{command}, @{method}, @{attribute} print checked |