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.32  
    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"