src/HOL/ex/MergeSort.thy
changeset 19872 1b53b196f85f
parent 19860 6e44610bdd76
child 29780 1df0e5af40b9
equal deleted inserted replaced
19871:88e8f6173bab 19872:1b53b196f85f
    49 by (induct xs rule: msort.induct) simp_all
    49 by (induct xs rule: msort.induct) simp_all
    50 
    50 
    51 theorem multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
    51 theorem multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
    52 apply (induct xs rule: msort.induct)
    52 apply (induct xs rule: msort.induct)
    53   apply simp_all
    53   apply simp_all
    54 apply (subst union_commute) back
    54 apply (subst union_commute)
    55 apply (simp del:multiset_of_append add:multiset_of_append[symmetric] union_assoc)
    55 apply (simp del:multiset_of_append add:multiset_of_append[symmetric] union_assoc)
    56 apply (simp add: union_ac)
    56 apply (simp add: union_ac)
    57 done
    57 done
    58 
    58 
    59 end
    59 end