src/HOL/Library/Multiset.thy
 changeset 64911 f0e07600de47 parent 64591 240a39af9ec4 child 65027 2b8583507891
1.1 --- a/src/HOL/Library/Multiset.thy	Tue Jan 17 11:26:21 2017 +0100
1.2 +++ b/src/HOL/Library/Multiset.thy	Tue Jan 17 13:59:10 2017 +0100
1.3 @@ -2805,7 +2805,7 @@
1.4      case (add z Z)
1.5      obtain X' Y' Z' where *: "add_mset z X + Z = Z' + X'" "add_mset z Y + Z = Z' + Y'" "Y' \<noteq> {#}"
1.6        "\<forall>x \<in> set_mset X'. \<exists>y \<in> set_mset Y'. (x, y) \<in> s"
1.7 -      using mult_implies_one_step[OF `trans s` add(2)] by auto
1.8 +      using mult_implies_one_step[OF \<open>trans s\<close> add(2)] by auto
1.9      consider Z2 where "Z' = add_mset z Z2" | X2 Y2 where "X' = add_mset z X2" "Y' = add_mset z Y2"
1.10        using *(1,2) by (metis add_mset_remove_trivial_If insert_iff set_mset_add_mset_insert union_iff)
1.11      thus ?case
1.12 @@ -2813,9 +2813,9 @@
1.13        case 1 thus ?thesis using * one_step_implies_mult[of Y' X' s Z2]
1.14          by (auto simp: add.commute[of _ "{#_#}"] add.assoc intro: add(1))
1.15      next
1.16 -      case 2 then obtain y where "y \<in> set_mset Y2" "(z, y) \<in> s" using *(4) `irrefl s`
1.17 +      case 2 then obtain y where "y \<in> set_mset Y2" "(z, y) \<in> s" using *(4) \<open>irrefl s\<close>
1.18          by (auto simp: irrefl_def)
1.19 -      moreover from this transD[OF `trans s` _ this(2)]
1.20 +      moreover from this transD[OF \<open>trans s\<close> _ this(2)]
1.21        have "x' \<in> set_mset X2 \<Longrightarrow> \<exists>y \<in> set_mset Y2. (x', y) \<in> s" for x'
1.22          using 2 *(4)[rule_format, of x'] by auto
1.23        ultimately show ?thesis using  * one_step_implies_mult[of Y2 X2 s Z'] 2
1.24 @@ -2825,7 +2825,7 @@
1.25  next
1.26    assume ?R then obtain I J K
1.27      where "Y = I + J" "X = I + K" "J \<noteq> {#}" "\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> s"
1.28 -    using mult_implies_one_step[OF `trans s`] by blast
1.29 +    using mult_implies_one_step[OF \<open>trans s\<close>] by blast
1.30    thus ?L using one_step_implies_mult[of J K s "I + Z"] by (auto simp: ac_simps)
1.31  qed
1.33 @@ -2887,7 +2887,7 @@
1.34  proof -
1.35    { assume "N \<noteq> M" "M - M \<inter># N = {#}"
1.36      then obtain y where "count N y \<noteq> count M y" by (auto simp: count_inject[symmetric])
1.37 -    then have "\<exists>y. count M y < count N y" using `M - M \<inter># N = {#}`
1.38 +    then have "\<exists>y. count M y < count N y" using \<open>M - M \<inter># N = {#}\<close>
1.39        by (auto simp: count_inject[symmetric] dest!: le_neq_implies_less fun_cong[of _ _ y])
1.40    }
1.41    then have "multeqp P N M \<longleftrightarrow> multp P N M \<or> N = M"