# HG changeset patch
# User wenzelm
# Date 1447324256 -3600
# Node ID 71da80a379c65103573e9feef534f5caa68551d4
# Parent  40ca618e1b2d349b7b9433d7677e08ee819ee5e6
support short form for \<^theory_text>;

diff -r 40ca618e1b2d -r 71da80a379c6 NEWS
--- a/NEWS	Wed Nov 11 19:22:18 2015 +0100
+++ b/NEWS	Thu Nov 12 11:30:56 2015 +0100
@@ -92,7 +92,8 @@
 symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>".
 
 * Antiquotation @{theory_text} prints uninterpreted theory source text
-(outer syntax with command keywords etc.).
+(outer syntax with command keywords etc.). This may be used in the short
+form \<^theory_text>\<open>...\<close>.
 
 * Antiquotations @{command}, @{method}, @{attribute} print checked
 entities of the Isar language.
@@ -133,11 +134,11 @@
 the lack of the surrounding isabelle markup environment in output.
 
 * Document antiquotations @{emph} and @{bold} output LaTeX source
-recursively, adding appropriate text style markup. These are typically
-used in the short form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>.
+recursively, adding appropriate text style markup. These may be used in
+the short form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>.
 
 * Document antiquotation @{footnote} outputs LaTeX source recursively,
-marked as \footnote{}. This is typically used in the short form \<^footnote>\<open>...\<close>.
+marked as \footnote{}. This may be used in the short form \<^footnote>\<open>...\<close>.
 
 
 *** Isar ***
diff -r 40ca618e1b2d -r 71da80a379c6 etc/symbols
--- a/etc/symbols	Wed Nov 11 19:22:18 2015 +0100
+++ b/etc/symbols	Thu Nov 12 11:30:56 2015 +0100
@@ -363,6 +363,7 @@
 \<^descr>               code: 0x0027a7  group: control  font: IsabelleText
 \<^footnote>            code: 0x00204b  group: control  font: IsabelleText
 \<^verbatim>            code: 0x0025a9  group: control  font: IsabelleText
+\<^theory_text>         code: 0x002b1a  group: control  font: IsabelleText
 \<^emph>                code: 0x002217  group: control  font: IsabelleText
 \<^bold>                code: 0x002759  group: control  font: IsabelleText
 \<^sub>                 code: 0x0021e9  group: control  font: IsabelleText