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.
corrected w.r.t. search order for subst.
authordixon
Tue, 13 Jun 2006 15:42:52 +0200
changeset 19872 1b53b196f85f
parent 19871 88e8f6173bab
child 19873 588329441a78
corrected w.r.t. search order for subst.
src/HOL/ex/MergeSort.thy file | annotate | diff | comparison | revisions 
--- 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