src/ZF/OrdQuant.thy
changeset 12763 6cecd9dfd53f
parent 12667 7e6eaaa125f2
child 12820 02e2ff3e4d37
     1.1 --- a/src/ZF/OrdQuant.thy	Tue Jan 15 10:23:58 2002 +0100
     1.2 +++ b/src/ZF/OrdQuant.thy	Tue Jan 15 10:24:20 2002 +0100
     1.3 @@ -148,4 +148,9 @@
     1.4        ==> (UN z < Union(X). C(z)) = (UN x:X. UN z < x. C(z))"
     1.5  by (simp add: OUnion_def) 
     1.6  
     1.7 +(*So that rule_format will get rid of ALL x<A...*)
     1.8 +lemma atomize_oall [symmetric, rulify]:
     1.9 +     "(!!x. x<A ==> P(x)) == Trueprop (ALL x<A. P(x))"
    1.10 +by (simp add: oall_def atomize_all atomize_imp)
    1.11 +
    1.12  end