equal
deleted
inserted
replaced
121 the lack of the surrounding isabelle markup environment in output. |
121 the lack of the surrounding isabelle markup environment in output. |
122 |
122 |
123 * Document antiquotations @{emph} and @{bold} output LaTeX source |
123 * Document antiquotations @{emph} and @{bold} output LaTeX source |
124 recursively, adding appropriate text style markup. These are typically |
124 recursively, adding appropriate text style markup. These are typically |
125 used in the short form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>. |
125 used in the short form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>. |
|
126 |
|
127 * Document antiquotation @{footnote} outputs LaTeX source recursively, |
|
128 marked as \footnote{}. This is typically used in the short form \<^footnote>\<open>...\<close>. |
126 |
129 |
127 |
130 |
128 *** Isar *** |
131 *** Isar *** |
129 |
132 |
130 * Command 'obtain' binds term abbreviations (via 'is' patterns) in the |
133 * Command 'obtain' binds term abbreviations (via 'is' patterns) in the |