# HG changeset patch
# User nipkow
# Date 1091804114 -7200
# Node ID f0359f75682e85d19069f65940e0ad0fb65c2cac
# Parent  e5f167042c1d3654ab73c5dcbde01d0d6b883427
undid UN/INT syntax

diff -r e5f167042c1d -r f0359f75682e src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Fri Aug 06 16:54:26 2004 +0200
+++ b/src/HOL/Algebra/Coset.thy	Fri Aug 06 16:55:14 2004 +0200
@@ -153,13 +153,13 @@
   proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify)
     fix x
     assume x: "x \<in> carrier G"
-    show "(\<Union>\<^bsub>h\<in>N\<^esub> {h \<otimes> x}) = (\<Union>\<^bsub>h\<in>N\<^esub> {x \<otimes> h})"
+    show "(\<Union>h\<in>N. {h \<otimes> x}) = (\<Union>h\<in>N. {x \<otimes> h})"
     proof
-      show "(\<Union>\<^bsub>h\<in>N\<^esub> {h \<otimes> x}) \<subseteq> (\<Union>\<^bsub>h\<in>N\<^esub> {x \<otimes> h})"
+      show "(\<Union>h\<in>N. {h \<otimes> x}) \<subseteq> (\<Union>h\<in>N. {x \<otimes> h})"
       proof clarify
         fix n
         assume n: "n \<in> N" 
-        show "n \<otimes> x \<in> (\<Union>\<^bsub>h\<in>N\<^esub> {x \<otimes> h})"
+        show "n \<otimes> x \<in> (\<Union>h\<in>N. {x \<otimes> h})"
         proof 
           from closed [of "inv x"]
           show "inv x \<otimes> n \<otimes> x \<in> N" by (simp add: x n)
@@ -168,11 +168,11 @@
         qed
       qed
     next
-      show "(\<Union>\<^bsub>h\<in>N\<^esub> {x \<otimes> h}) \<subseteq> (\<Union>\<^bsub>h\<in>N\<^esub> {h \<otimes> x})"
+      show "(\<Union>h\<in>N. {x \<otimes> h}) \<subseteq> (\<Union>h\<in>N. {h \<otimes> x})"
       proof clarify
         fix n
         assume n: "n \<in> N" 
-        show "x \<otimes> n \<in> (\<Union>\<^bsub>h\<in>N\<^esub> {h \<otimes> x})"
+        show "x \<otimes> n \<in> (\<Union>h\<in>N. {h \<otimes> x})"
         proof 
           show "x \<otimes> n \<otimes> inv x \<in> N" by (simp add: x n closed)
           show "x \<otimes> n \<in> {x \<otimes> n \<otimes> inv x \<otimes> x}"
@@ -261,7 +261,7 @@
 proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe)
   fix h
   assume "h \<in> H"
-  show "inv x \<otimes> inv h \<in> (\<Union>\<^bsub>j\<in>H\<^esub> {j \<otimes> inv x})"
+  show "inv x \<otimes> inv h \<in> (\<Union>j\<in>H. {j \<otimes> inv x})"
   proof
     show "inv x \<otimes> inv h \<otimes> x \<in> H"
       by (simp add: inv_op_closed1 prems)
@@ -271,7 +271,7 @@
 next
   fix h
   assume "h \<in> H"
-  show "h \<otimes> inv x \<in> (\<Union>\<^bsub>j\<in>H\<^esub> {inv x \<otimes> inv j})"
+  show "h \<otimes> inv x \<in> (\<Union>j\<in>H. {inv x \<otimes> inv j})"
   proof
     show "x \<otimes> inv h \<otimes> inv x \<in> H"
       by (simp add: inv_op_closed2 prems)
@@ -651,7 +651,7 @@
     assume y: "y \<in> carrier H"
     with h obtain g where g: "g \<in> carrier G" "h g = y"
       by (blast elim: equalityE); 
-    hence "(\<Union>\<^bsub>x\<in>kernel G H h #> g\<^esub> {h x}) = {y}" 
+    hence "(\<Union>x\<in>kernel G H h #> g. {h x}) = {y}" 
       by (auto simp add: y kernel_def r_coset_def) 
     with g show "y \<in> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)" 
       by (auto intro!: bexI simp add: FactGroup_def RCOSETS_def image_eq_UN)
diff -r e5f167042c1d -r f0359f75682e src/HOL/Induct/QuoDataType.thy
--- a/src/HOL/Induct/QuoDataType.thy	Fri Aug 06 16:54:26 2004 +0200
+++ b/src/HOL/Induct/QuoDataType.thy	Fri Aug 06 16:55:14 2004 +0200
@@ -147,15 +147,15 @@
 
   MPair :: "[msg,msg] \<Rightarrow> msg"
    "MPair X Y ==
-       Abs_Msg (\<Union>\<^bsub>U \<in> Rep_Msg X\<^esub> \<Union>\<^bsub>V \<in> Rep_Msg Y\<^esub> msgrel``{MPAIR U V})"
+       Abs_Msg (\<Union>U \<in> Rep_Msg X. \<Union>V \<in> Rep_Msg Y. msgrel``{MPAIR U V})"
 
   Crypt :: "[nat,msg] \<Rightarrow> msg"
    "Crypt K X ==
-       Abs_Msg (\<Union>\<^bsub>U \<in> Rep_Msg X\<^esub> msgrel``{CRYPT K U})"
+       Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{CRYPT K U})"
 
   Decrypt :: "[nat,msg] \<Rightarrow> msg"
    "Decrypt K X ==
-       Abs_Msg (\<Union>\<^bsub>U \<in> Rep_Msg X\<^esub> msgrel``{DECRYPT K U})"
+       Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{DECRYPT K U})"
 
 
 text{*Reduces equality of equivalence classes to the @{term msgrel} relation:
@@ -228,7 +228,7 @@
 
 constdefs
   nonces :: "msg \<Rightarrow> nat set"
-   "nonces X == \<Union>\<^bsub>U \<in> Rep_Msg X\<^esub> freenonces U"
+   "nonces X == \<Union>U \<in> Rep_Msg X. freenonces U"
 
 lemma nonces_congruent: "congruent msgrel freenonces"
 by (simp add: congruent_def msgrel_imp_eq_freenonces) 
@@ -263,7 +263,7 @@
 
 constdefs
   left :: "msg \<Rightarrow> msg"
-   "left X == Abs_Msg (\<Union>\<^bsub>U \<in> Rep_Msg X\<^esub> msgrel``{freeleft U})"
+   "left X == Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeleft U})"
 
 lemma left_congruent: "congruent msgrel (\<lambda>U. msgrel `` {freeleft U})"
 by (simp add: congruent_def msgrel_imp_eqv_freeleft) 
@@ -297,7 +297,7 @@
 
 constdefs
   right :: "msg \<Rightarrow> msg"
-   "right X == Abs_Msg (\<Union>\<^bsub>U \<in> Rep_Msg X\<^esub> msgrel``{freeright U})"
+   "right X == Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeright U})"
 
 lemma right_congruent: "congruent msgrel (\<lambda>U. msgrel `` {freeright U})"
 by (simp add: congruent_def msgrel_imp_eqv_freeright) 
diff -r e5f167042c1d -r f0359f75682e src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Aug 06 16:54:26 2004 +0200
+++ b/src/HOL/Set.thy	Fri Aug 06 16:55:14 2004 +0200
@@ -120,17 +120,30 @@
   "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
   "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
 
-syntax (input)
+syntax (xsymbols)
   "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" 10)
   "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" 10)
   "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" 10)
   "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" 10)
-
+(*
 syntax (xsymbols)
   "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" 10)
   "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" 10)
   "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
   "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
+*)
+syntax (latex output)
+  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" 10)
+  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" 10)
+  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
+  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
+
+text{* Note the difference between ordinary xsymbol syntax of indexed
+unions and intersections (e.g.\ @{text"\<Union>a\<^isub>1\<in>A\<^isub>1. B"})
+and their \LaTeX\ rendition: @{term"\<Union>a\<^isub>1\<in>A\<^isub>1. B"}. The
+former does not make the index expression a subscript of the
+union/intersection symbol because this leads to problems with nested
+subscripts in Proof General.  *}
 
 
 translations