now [rule_format] knows about ospec
authorpaulson
Tue Jan 15 10:24:20 2002 +0100 (2002-01-15)
changeset 127636cecd9dfd53f
parent 12762 a0c0a1e3a53a
child 12764 b43333dc6e7d
now [rule_format] knows about ospec
src/ZF/OrdQuant.thy
     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