src/HOL/ex/MergeSort.thy
changeset 19860 6e44610bdd76
parent 15815 62854cac5410
child 19872 1b53b196f85f
     1.1 --- a/src/HOL/ex/MergeSort.thy	Mon Jun 12 20:58:25 2006 +0200
     1.2 +++ b/src/HOL/ex/MergeSort.thy	Mon Jun 12 21:18:10 2006 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4  theorem multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
     1.5  apply (induct xs rule: msort.induct)
     1.6    apply simp_all
     1.7 -apply (subst union_commute)
     1.8 +apply (subst union_commute) back
     1.9  apply (simp del:multiset_of_append add:multiset_of_append[symmetric] union_assoc)
    1.10  apply (simp add: union_ac)
    1.11  done