88 that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and |
88 that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and |
89 \<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}. |
89 \<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}. |
90 \<^name> without following cartouche is equivalent to @{name}. The |
90 \<^name> without following cartouche is equivalent to @{name}. The |
91 standard Isabelle fonts provide glyphs to render important control |
91 standard Isabelle fonts provide glyphs to render important control |
92 symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>". |
92 symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>". |
|
93 |
|
94 * Antiquotation @{theory_text} prints uninterpreted theory source text |
|
95 (outer syntax with command keywords etc.). |
93 |
96 |
94 * Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with |
97 * Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with |
95 corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using |
98 corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using |
96 standard LaTeX macros of the same names. |
99 standard LaTeX macros of the same names. |
97 |
100 |