--- 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);