now [rule_format] knows about ospec

--- a/src/ZF/OrdQuant.thy	Tue Jan 15 10:23:58 2002 +0100
+++ b/src/ZF/OrdQuant.thy	Tue Jan 15 10:24:20 2002 +0100
@@ -148,4 +148,9 @@
       ==> (UN z < Union(X). C(z)) = (UN x:X. UN z < x. C(z))"
 by (simp add: OUnion_def) 
 
+(*So that rule_format will get rid of ALL x<A...*)
+lemma atomize_oall [symmetric, rulify]:
+     "(!!x. x<A ==> P(x)) == Trueprop (ALL x<A. P(x))"
+by (simp add: oall_def atomize_all atomize_imp)
+
 end