src/HOL/BNF_Wellorder_Embedding.thy
changeset 55811 aa1acc25126b
parent 55101 57c875e488bd
child 55936 f6591f8c629d
--- a/src/HOL/BNF_Wellorder_Embedding.thy	Fri Feb 28 22:00:13 2014 +0100
+++ b/src/HOL/BNF_Wellorder_Embedding.thy	Fri Feb 28 17:54:52 2014 +0100
@@ -305,8 +305,7 @@
   (* Main proof *)
   show "bij_betw f (under r a) (under r' (f a))"
   proof(unfold bij_betw_def, auto)
-    show  "inj_on f (under r a)"
-    using * by (metis (no_types) under_Field subset_inj_on)
+    show  "inj_on f (under r a)" by (rule subset_inj_on[OF * under_Field])
   next
     fix b assume "b \<in> under r a"
     thus "f b \<in> under r' (f a)"
@@ -1035,8 +1034,7 @@
   {fix a assume ***: "a \<in> Field r"
    have "bij_betw f (under r a) (under r' (f a))"
    proof(unfold bij_betw_def, auto)
-     show "inj_on f (under r a)"
-     using 1 2 by (metis subset_inj_on)
+     show "inj_on f (under r a)" using 1 2 subset_inj_on by blast
    next
      fix b assume "b \<in> under r a"
      hence "a \<in> Field r \<and> b \<in> Field r \<and> (b,a) \<in> r"