src/HOL/Equiv_Relations.thy
changeset 61952 546958347e05
parent 61799 4cf66f21b764
child 63092 a949b2a5f51d
     1.1 --- a/src/HOL/Equiv_Relations.thy	Mon Dec 28 16:34:26 2015 +0100
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Mon Dec 28 17:43:30 2015 +0100
     1.3 @@ -108,7 +108,7 @@
     1.4    "X \<in> A//r ==> (!!x. X = r``{x} ==> x \<in> A ==> P) ==> P"
     1.5    by (unfold quotient_def) blast
     1.6  
     1.7 -lemma Union_quotient: "equiv A r ==> Union (A//r) = A"
     1.8 +lemma Union_quotient: "equiv A r ==> \<Union>(A//r) = A"
     1.9    by (unfold equiv_def refl_on_def quotient_def) blast
    1.10  
    1.11  lemma quotient_disj: