# HG changeset patch
# User wenzelm
# Date 1444662636 -7200
# Node ID d2ce32c5793a5e818acb7cc5264cc14f9a5e33cf
# Parent  a433fecc5ce26d381f5039777960c5a3e75e7126
some control symbols for markup and formatting;

diff -r a433fecc5ce2 -r d2ce32c5793a NEWS
--- a/NEWS	Mon Oct 12 17:06:49 2015 +0200
+++ b/NEWS	Mon Oct 12 17:10:36 2015 +0200
@@ -55,6 +55,18 @@
 requirements of prover time and GUI space.
 
 
+*** Document preparation ***
+
+* Isabelle control symbols for markup and formatting:
+
+  \<^smallskip>   \smallskip
+  \<^medskip>   \medskip
+  \<^bigskip>   \bigskip
+
+  \<^item>  \item  (itemize)
+  \<^enum>  \item  (enumeration)
+
+
 *** Isar ***
 
 * Command 'obtain' binds term abbreviations (via 'is' patterns) in the
diff -r a433fecc5ce2 -r d2ce32c5793a etc/symbols
--- a/etc/symbols	Mon Oct 12 17:06:49 2015 +0200
+++ b/etc/symbols	Mon Oct 12 17:10:36 2015 +0200
@@ -359,3 +359,8 @@
 \<^esub>                code: 0x0021d9  group: control_block  font: IsabelleText  abbrev: =_)
 \<^bsup>                code: 0x0021d7  group: control_block  font: IsabelleText  abbrev: =^(
 \<^esup>                code: 0x0021d6  group: control_block  font: IsabelleText  abbrev: =^)
+\<^smallskip>           code: 0x002508  group: control
+\<^medskip>             code: 0x002509  group: control
+\<^bigskip>             code: 0x002501  group: control
+\<^item>                code: 0x0025aa  group: control
+\<^enum>                code: 0x0025b8  group: control
diff -r a433fecc5ce2 -r d2ce32c5793a lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Mon Oct 12 17:06:49 2015 +0200
+++ b/lib/texinputs/isabelle.sty	Mon Oct 12 17:10:36 2015 +0200
@@ -39,6 +39,12 @@
 \DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 
+\def\isactrlsmallskip{\smallskip}
+\def\isactrlmedskip{\medskip}
+\def\isactrlbigskip{\bigskip}
+\def\isactrlitem{\item}
+\def\isactrlenum{\item}
+
 \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
 
 \newdimen\isa@parindent\newdimen\isa@parskip