src/HOL/ZF/LProd.thy
changeset 62651 66568c9b8216
parent 60515 484559628038
child 66453 cc19f7ca2ed6
--- a/src/HOL/ZF/LProd.thy	Fri Mar 18 10:14:56 2016 +0100
+++ b/src/HOL/ZF/LProd.thy	Fri Mar 18 12:48:00 2016 +0100
@@ -59,7 +59,7 @@
   proof (cases "a = b")
     case True    
     have "((I + {#b#}) + K, (I + {#b#}) + J) \<in> mult R"
-      apply (rule one_step_implies_mult[OF transR])
+      apply (rule one_step_implies_mult)
       apply (auto simp add: decomposed)
       done
     then show ?thesis
@@ -71,7 +71,7 @@
     case False
     from False lprod_list have False: "(a, b) \<in> R" by blast
     have "(I + (K + {#a#}), I + (J + {#b#})) \<in> mult R"
-      apply (rule one_step_implies_mult[OF transR])
+      apply (rule one_step_implies_mult)
       apply (auto simp add: False decomposed)
       done
     then show ?thesis