--- a/src/HOL/ex/InSort.ML Fri Jan 17 18:50:04 1997 +0100
+++ b/src/HOL/ex/InSort.ML Fri Jan 17 19:26:47 1997 +0100
@@ -6,8 +6,6 @@
Correctness proof of insertion sort.
*)
-Addsimps [Ball_insert];
-
goal thy "!y. mset(ins f x xs) y = mset (x#xs) y";
by (list.induct_tac "xs" 1);
by (Asm_simp_tac 1);
--- a/src/HOL/ex/Qsort.ML Fri Jan 17 18:50:04 1997 +0100
+++ b/src/HOL/ex/Qsort.ML Fri Jan 17 19:26:47 1997 +0100
@@ -6,8 +6,7 @@
Two verifications of Quicksort
*)
-
-Addsimps [Ball_insert,Ball_Un];
+Addsimps [ball_Un];
(* Towards a proof of qsort_ind