\<^bsub>/\<^esub> syntax: unbreakable block;
authorwenzelm
Sat May 29 16:47:06 2004 +0200 (2004-05-29)
changeset 14846b1fcade3880b
parent 14845 345934d5bc1a
child 14847 44d92c12b255
\<^bsub>/\<^esub> syntax: unbreakable block;
src/HOL/SetInterval.thy
src/Pure/Syntax/mixfix.ML
     1.1 --- a/src/HOL/SetInterval.thy	Sat May 29 15:11:43 2004 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Sat May 29 16:47:06 2004 +0200
     1.3 @@ -49,10 +49,10 @@
     1.4    "@INTER_less" :: "nat => nat => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" 10)
     1.5  
     1.6  syntax (xsymbols)
     1.7 -  "@UNION_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>()\<^bsub>_ \<le> _\<^esub>/ _)" 10)
     1.8 -  "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>()\<^bsub>_ < _\<^esub>/ _)" 10)
     1.9 -  "@INTER_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>()\<^bsub>_ \<le> _\<^esub>/ _)" 10)
    1.10 -  "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>()\<^bsub>_ < _\<^esub>/ _)" 10)
    1.11 +  "@UNION_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>(00\<^bsub>_ \<le> _\<^esub>)/ _)" 10)
    1.12 +  "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>(00\<^bsub>_ < _\<^esub>)/ _)" 10)
    1.13 +  "@INTER_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>(00\<^bsub>_ \<le> _\<^esub>)/ _)" 10)
    1.14 +  "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>(00\<^bsub>_ < _\<^esub>)/ _)" 10)
    1.15  
    1.16  translations
    1.17    "UN i<=n. A"  == "UN i:{..n}. A"
     2.1 --- a/src/Pure/Syntax/mixfix.ML	Sat May 29 15:11:43 2004 +0200
     2.2 +++ b/src/Pure/Syntax/mixfix.ML	Sat May 29 16:47:06 2004 +0200
     2.3 @@ -240,7 +240,7 @@
     2.4    ("_DDDOT",      "logic",                     Delimfix "..."),
     2.5    ("_constify",   "num => num_const",          Delimfix "_"),
     2.6    ("_indexnum",   "num_const => index",        Delimfix "\\<^sub>_"),
     2.7 -  ("_index",      "logic => index",            Delimfix "\\<^bsub>_\\<^esub>"),
     2.8 +  ("_index",      "logic => index",            Delimfix "(00\\<^bsub>_\\<^esub>)"),
     2.9    ("_indexdefault", "index",                   Delimfix ""),
    2.10    ("_indexvar",   "index",                     Delimfix "'\\<index>"),
    2.11    ("_struct",     "index => logic",            Mixfix ("\\<struct>_", [1000], 1000))];