src/ZF/OrdQuant.thy
changeset 58860 fee7cfa69c50
parent 56250 2c9f841f36b8
child 58871 c399ae4b836f
     1.1 --- a/src/ZF/OrdQuant.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/ZF/OrdQuant.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -273,7 +273,7 @@
     1.4  lemma rex_is_bex [simp]: "(\<exists>x[%z. z\<in>A]. P(x)) <-> (\<exists>x\<in>A. P(x))"
     1.5  by blast
     1.6  
     1.7 -lemma atomize_rall: "(!!x. M(x) ==> P(x)) == Trueprop (\<forall>x[M]. P(x))";
     1.8 +lemma atomize_rall: "(!!x. M(x) ==> P(x)) == Trueprop (\<forall>x[M]. P(x))"
     1.9  by (simp add: rall_def atomize_all atomize_imp)
    1.10  
    1.11  declare atomize_rall [symmetric, rulify]