# HG changeset patch
# User paulson
# Date 1011086660 -3600
# Node ID 6cecd9dfd53f4554e9916d6ae3637deaa6e1df4d
# Parent  a0c0a1e3a53add355dc14e348762bd1f67418e9a
now [rule_format] knows about ospec

diff -r a0c0a1e3a53a -r 6cecd9dfd53f src/ZF/OrdQuant.thy
--- 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