src/ZF/UNITY/Union.thy
changeset 45602 2a858377c3d2
parent 35427 ad039d29e01c
child 46823 57bf0cecb366
     1.1 --- a/src/ZF/UNITY/Union.thy	Sun Nov 20 17:57:09 2011 +0100
     1.2 +++ b/src/ZF/UNITY/Union.thy	Sun Nov 20 20:15:02 2011 +0100
     1.3 @@ -427,7 +427,7 @@
     1.4  lemma ok_commute: "(F ok G) <->(G ok F)"
     1.5  by (auto simp add: ok_def)
     1.6  
     1.7 -lemmas ok_sym = ok_commute [THEN iffD1, standard]
     1.8 +lemmas ok_sym = ok_commute [THEN iffD1]
     1.9  
    1.10  lemma ok_iff_OK: "OK({<0,F>,<1,G>,<2,H>}, snd) <-> (F ok G & (F Join G) ok H)"
    1.11  by (simp add: ok_def Join_def OK_def Int_assoc cons_absorb