src/HOL/Library/Multiset_Order.thy
changeset 63040 eb4ddd18d635
parent 62430 9527ff088c15
child 63310 caaacf37943f
     1.1 --- a/src/HOL/Library/Multiset_Order.thy	Sun Apr 24 21:31:14 2016 +0200
     1.2 +++ b/src/HOL/Library/Multiset_Order.thy	Mon Apr 25 16:09:26 2016 +0200
     1.3 @@ -157,8 +157,8 @@
     1.4    assume "less_multiset\<^sub>H\<^sub>O M N"
     1.5    then obtain z where z: "count M z < count N z"
     1.6      unfolding less_multiset\<^sub>H\<^sub>O_def by (auto simp: multiset_eq_iff nat_neq_iff)
     1.7 -  def X \<equiv> "N - M"
     1.8 -  def Y \<equiv> "M - N"
     1.9 +  define X where "X = N - M"
    1.10 +  define Y where "Y = M - N"
    1.11    from z show "X \<noteq> {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq)
    1.12    from z show "X \<le># N" unfolding X_def by auto
    1.13    show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force