Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/MergeSort.thy
changeset 19872 1b53b196f85f
parent 19860 6e44610bdd76
child 29780 1df0e5af40b9 
--- a/src/HOL/ex/MergeSort.thy	Tue Jun 13 15:42:19 2006 +0200
+++ b/src/HOL/ex/MergeSort.thy	Tue Jun 13 15:42:52 2006 +0200
@@ -51,7 +51,7 @@
 theorem multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
 apply (induct xs rule: msort.induct)
   apply simp_all
-apply (subst union_commute) back
+apply (subst union_commute)
 apply (simp del:multiset_of_append add:multiset_of_append[symmetric] union_assoc)
 apply (simp add: union_ac)
 done
isabelle