# HG changeset patch
# User wenzelm
# Date 1085842026 -7200
# Node ID b1fcade3880be2e3aefe0bdd1be2b299af2b725d
# Parent  345934d5bc1aebd2cbe070f1021ea654d5c69be0
\<^bsub>/\<^esub> syntax: unbreakable block;

diff -r 345934d5bc1a -r b1fcade3880b src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Sat May 29 15:11:43 2004 +0200
+++ b/src/HOL/SetInterval.thy	Sat May 29 16:47:06 2004 +0200
@@ -49,10 +49,10 @@
   "@INTER_less" :: "nat => nat => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" 10)
 
 syntax (xsymbols)
-  "@UNION_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>()\<^bsub>_ \<le> _\<^esub>/ _)" 10)
-  "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>()\<^bsub>_ < _\<^esub>/ _)" 10)
-  "@INTER_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>()\<^bsub>_ \<le> _\<^esub>/ _)" 10)
-  "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>()\<^bsub>_ < _\<^esub>/ _)" 10)
+  "@UNION_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>(00\<^bsub>_ \<le> _\<^esub>)/ _)" 10)
+  "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>(00\<^bsub>_ < _\<^esub>)/ _)" 10)
+  "@INTER_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>(00\<^bsub>_ \<le> _\<^esub>)/ _)" 10)
+  "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>(00\<^bsub>_ < _\<^esub>)/ _)" 10)
 
 translations
   "UN i<=n. A"  == "UN i:{..n}. A"
diff -r 345934d5bc1a -r b1fcade3880b src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Sat May 29 15:11:43 2004 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Sat May 29 16:47:06 2004 +0200
@@ -240,7 +240,7 @@
   ("_DDDOT",      "logic",                     Delimfix "..."),
   ("_constify",   "num => num_const",          Delimfix "_"),
   ("_indexnum",   "num_const => index",        Delimfix "\\<^sub>_"),
-  ("_index",      "logic => index",            Delimfix "\\<^bsub>_\\<^esub>"),
+  ("_index",      "logic => index",            Delimfix "(00\\<^bsub>_\\<^esub>)"),
   ("_indexdefault", "index",                   Delimfix ""),
   ("_indexvar",   "index",                     Delimfix "'\\<index>"),
   ("_struct",     "index => logic",            Mixfix ("\\<struct>_", [1000], 1000))];