corrected w.r.t. search order for subst.
authordixon
Tue Jun 13 15:42:52 2006 +0200 (2006-06-13)
changeset 198721b53b196f85f
parent 19871 88e8f6173bab
child 19873 588329441a78
corrected w.r.t. search order for subst.
src/HOL/ex/MergeSort.thy
     1.1 --- a/src/HOL/ex/MergeSort.thy	Tue Jun 13 15:42:19 2006 +0200
     1.2 +++ b/src/HOL/ex/MergeSort.thy	Tue Jun 13 15:42:52 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) back
     1.8 +apply (subst union_commute)
     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