equal
deleted
inserted
replaced
92 symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>". |
92 symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>". |
93 |
93 |
94 * Antiquotation @{theory_text} prints uninterpreted theory source text |
94 * Antiquotation @{theory_text} prints uninterpreted theory source text |
95 (outer syntax with command keywords etc.). This may be used in the short |
95 (outer syntax with command keywords etc.). This may be used in the short |
96 form \<^theory_text>\<open>...\<close>. |
96 form \<^theory_text>\<open>...\<close>. |
|
97 |
|
98 * Antiquotation @{doc ENTRY} provides a reference to the given |
|
99 documentation, with a hyperlink in the Prover IDE. |
97 |
100 |
98 * Antiquotations @{command}, @{method}, @{attribute} print checked |
101 * Antiquotations @{command}, @{method}, @{attribute} print checked |
99 entities of the Isar language. |
102 entities of the Isar language. |
100 |
103 |
101 * Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with |
104 * Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with |