--- a/src/HOL/ex/Sorting.ML Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/ex/Sorting.ML Mon Jun 22 17:26:46 1998 +0200
@@ -6,12 +6,12 @@
Some general lemmas
*)
-goal Sorting.thy "!x. mset (xs@ys) x = mset xs x + mset ys x";
+Goal "!x. mset (xs@ys) x = mset xs x + mset ys x";
by (list.induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "mset_append";
-goal Sorting.thy "!x. mset [x:xs. ~p(x)] x + mset [x:xs. p(x)] x = \
+Goal "!x. mset [x:xs. ~p(x)] x + mset [x:xs. p(x)] x = \
\ mset xs x";
by (list.induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
@@ -19,7 +19,7 @@
Addsimps [mset_append, mset_compl_add];
-goal Sorting.thy "set xs = {x. mset xs x ~= 0}";
+Goal "set xs = {x. mset xs x ~= 0}";
by (list.induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
by (Fast_tac 1);