--- a/src/HOL/Library/Multiset.thy Fri Mar 18 10:14:56 2016 +0100
+++ b/src/HOL/Library/Multiset.thy Fri Mar 18 12:48:00 2016 +0100
@@ -2062,7 +2062,7 @@
done
lemma one_step_implies_mult:
- "trans r \<Longrightarrow> J \<noteq> {#} \<Longrightarrow> \<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r
+ "J \<noteq> {#} \<Longrightarrow> \<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r
\<Longrightarrow> (I + K, I + J) \<in> mult r"
using one_step_implies_mult_aux by blast
--- 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