author | paulson |
Mon, 20 Mar 2000 10:32:02 +0100 | |
changeset 8525 | 209eb2db72e6 |
parent 8524 | f990040535c9 |
child 8526 | 0be2c98f15a7 |
--- 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";