Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed subst step;
authorwenzelm
Mon, 12 Jun 2006 21:18:10 +0200
changeset 19860 6e44610bdd76
parent 19859 e5c12b5cb940
child 19861 620d90091788
fixed subst step;
src/HOL/ex/MergeSort.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/ex/MergeSort.thy	Mon Jun 12 20:58:25 2006 +0200
+++ b/src/HOL/ex/MergeSort.thy	Mon Jun 12 21:18:10 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)
+apply (subst union_commute) back
 apply (simp del:multiset_of_append add:multiset_of_append[symmetric] union_assoc)
 apply (simp add: union_ac)
 done
isabelle