--- 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"
--- 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))];