src/ZF/OrdQuant.thy
changeset 13339 0f89104dd377
parent 13302 98ce70e7d1f7
child 13362 cd7f9ea58338
     1.1 --- a/src/ZF/OrdQuant.thy	Wed Jul 10 16:07:52 2002 +0200
     1.2 +++ b/src/ZF/OrdQuant.thy	Wed Jul 10 16:54:07 2002 +0200
     1.3 @@ -232,8 +232,7 @@
     1.4  
     1.5  (*Congruence rule for rewriting*)
     1.6  lemma rall_cong [cong]:
     1.7 -    "(!!x. M(x) ==> P(x) <-> P'(x))
     1.8 -     ==> rall(M, %x. P(x)) <-> rall(M, %x. P'(x))"
     1.9 +    "(!!x. M(x) ==> P(x) <-> P'(x)) ==> (ALL x[M]. P(x)) <-> (ALL x[M]. P'(x))"
    1.10  by (simp add: rall_def)
    1.11  
    1.12  
    1.13 @@ -258,8 +257,7 @@
    1.14  by (simp add: rex_def)
    1.15  
    1.16  lemma rex_cong [cong]:
    1.17 -    "(!!x. M(x) ==> P(x) <-> P'(x))
    1.18 -     ==> rex(M, %x. P(x)) <-> rex(M, %x. P'(x))"
    1.19 +    "(!!x. M(x) ==> P(x) <-> P'(x)) ==> (EX x[M]. P(x)) <-> (EX x[M]. P'(x))"
    1.20  by (simp add: rex_def cong: conj_cong)
    1.21  
    1.22  lemma rall_is_ball [simp]: "(\<forall>x[%z. z\<in>A]. P(x)) <-> (\<forall>x\<in>A. P(x))"