src/ZF/Order.thy
changeset 59788 6f7b6adac439
parent 58871 c399ae4b836f
child 60770 240563fbf41d
     1.1 --- a/src/ZF/Order.thy	Mon Mar 23 19:43:03 2015 +0100
     1.2 +++ b/src/ZF/Order.thy	Mon Mar 23 21:05:17 2015 +0100
     1.3 @@ -670,8 +670,8 @@
     1.4    apply (auto simp: subset_def preorder_on_def refl_def vimage_def image_def)
     1.5     apply blast
     1.6    unfolding trans_on_def
     1.7 -  apply (erule_tac P = "(\<lambda>x. \<forall>y\<in>field(?r).
     1.8 -          \<forall>z\<in>field(?r). \<langle>x, y\<rangle> \<in> ?r \<longrightarrow> \<langle>y, z\<rangle> \<in> ?r \<longrightarrow> \<langle>x, z\<rangle> \<in> ?r)" in rev_ballE)
     1.9 +  apply (erule_tac P = "(\<lambda>x. \<forall>y\<in>field(r).
    1.10 +          \<forall>z\<in>field(r). \<langle>x, y\<rangle> \<in> r \<longrightarrow> \<langle>y, z\<rangle> \<in> r \<longrightarrow> \<langle>x, z\<rangle> \<in> r)" for r in rev_ballE)
    1.11      (* instance obtained from proof term generated by best *)
    1.12     apply best
    1.13    apply blast