Minor rearrange

1 files changed, 10 insertions, 9 deletions

diff --git a/etc/isar/TokensAcid.thy b/etc/isar/TokensAcid.thy
index 631ef336..30807b89 100644
--- a/etc/isar/TokensAcid.thy
+++ b/etc/isar/TokensAcid.thy
@@ -112,9 +112,6 @@ by auto
    See Tokens -> Format Char -> ...
 *)
 
-(*   NB: below here cannot be processed: just in terms to check with 
-     string font for terms. *)
-
 consts shortsub :: "['a,'a]\<Rightarrow>'a" ("_\<^sub>_")
 consts shortsup :: "['a,'a]\<Rightarrow>'a" ("_\<^sup>_")
 
@@ -136,11 +133,6 @@ term "a\<^isub>def"  (* no subscript on ef *)
 term "a\<^isub>x\<^isub>y"      (* x and y subscripted individually *)
 term "a\<^isub>xabc\<^isub>y"   (* x and y should be subscripted, but not ab *)
 
-(* Spanning identifier supers/subs: to be added to Isabelle lexer/latex *)
-
-term "a\<^bisup>bcd\<^eisup>"
-term "a\<^bisub>bcd\<^eisub>"
-
 (* 
    Variants on token names: different token names,
    same appearance.   Simulated overloading, \<^bitalic>much\<^eitalic> simpler to do
@@ -173,12 +165,21 @@ term "\<And2> {\<lambda> x. True, \<lambda> y. False}"
 
 
 
+(*   NB: below here cannot be processed: just in terms to check with 
+     string font for terms. *)
+
+
+(* Spanning identifier supers/subs: to be added to Isabelle lexer/latex *)
+
+term "a\<^bisup>bcd\<^eisup>"
+term "a\<^bisub>bcd\<^eisub>"
+
 (* More esoteric stuff *)
 
 
 term "\<^bbig>large text \<alpha> \<beta> \<Sigma>\<^ebig>"
 
-term "\<^bsmall>small\<^esmall>"
+term "\<^bsmall>small text \<alpha> \<and> \<beta> \<longrightarrow> \<gamma> \<^esmall>"
 
 term "\<^bunderline>underlined\<^eunderline>"