equal
deleted
inserted
replaced
60 |
60 |
61 *** Document preparation *** |
61 *** Document preparation *** |
62 |
62 |
63 * There is a new short form for antiquotations with a single argument |
63 * There is a new short form for antiquotations with a single argument |
64 that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and |
64 that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and |
65 \<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}. |
65 \<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}. The |
|
66 standard Isabelle fonts provide glyphs to render important control |
|
67 symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>". |
66 |
68 |
67 * Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}. |
69 * Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}. |
68 Consequently, \<open>...\<close> without any decoration prints literal quasi-formal |
70 Consequently, \<open>...\<close> without any decoration prints literal quasi-formal |
69 text. Command-line tool "isabelle update_cartouches -t" helps to update |
71 text. Command-line tool "isabelle update_cartouches -t" helps to update |
70 old sources, by approximative patching of the content of string and |
72 old sources, by approximative patching of the content of string and |