equal
deleted
inserted
replaced
20 accordingly. |
20 accordingly. |
21 |
21 |
22 * Toplevel theorem statement 'proposition' is another alias for |
22 * Toplevel theorem statement 'proposition' is another alias for |
23 'theorem'. |
23 'theorem'. |
24 |
24 |
25 * There is a new short form of antiquotations: \<^foo>\<open>...\<close> is |
25 * There is a new short form for antiquotations with a single argument |
26 equivalent to @{"\<^foo>" \<open>...\<close>} for control symbols. |
26 that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>}. |
27 |
27 |
28 |
28 |
29 *** Prover IDE -- Isabelle/Scala/jEdit *** |
29 *** Prover IDE -- Isabelle/Scala/jEdit *** |
30 |
30 |
31 * Improved scheduling for urgent print tasks (e.g. command state output, |
31 * Improved scheduling for urgent print tasks (e.g. command state output, |
79 \<^bigskip> \bigskip |
79 \<^bigskip> \bigskip |
80 |
80 |
81 * Command 'text_raw' has been clarified: input text is processed as in |
81 * Command 'text_raw' has been clarified: input text is processed as in |
82 'text' (with antiquotations and control symbols). The key difference is |
82 'text' (with antiquotations and control symbols). The key difference is |
83 the lack of the surrounding isabelle markup environment in output. |
83 the lack of the surrounding isabelle markup environment in output. |
|
84 |
|
85 * Document antiquotations @{emph} and @{bold} output LaTeX source |
|
86 recursively, adding appropriate text style markup. These are typically |
|
87 used in the short form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>. |
84 |
88 |
85 |
89 |
86 *** Isar *** |
90 *** Isar *** |
87 |
91 |
88 * Command 'obtain' binds term abbreviations (via 'is' patterns) in the |
92 * Command 'obtain' binds term abbreviations (via 'is' patterns) in the |