src/HOL/ex/Sorting.ML
changeset 8525 209eb2db72e6
parent 8415 852c63072334
child 12486 0ed8bdd883e0
--- a/src/HOL/ex/Sorting.ML	Mon Mar 20 10:26:34 2000 +0100
+++ b/src/HOL/ex/Sorting.ML	Mon Mar 20 10:32:02 2000 +0100
@@ -11,7 +11,7 @@
 by Auto_tac;
 qed "multiset_append";
 
-Goal "multiset [x:xs. ~p(x)] x + multiset [x:xs. p(x)] x = multiset xs x";
+Goal "multiset [x:xs. ~p(x)] z + multiset [x:xs. p(x)] z = multiset xs z";
 by (induct_tac "xs" 1);
 by Auto_tac;
 qed "multiset_compl_add";