# HG changeset patch
# User nipkow
# Date 853525607 -3600
# Node ID 43650141d67d0cd36312f4c72d2a9003d59d7671
# Parent  477c055862862ea1b0f4e32679d7283c9c978ee2
Ball_Un -> ball_Un

diff -r 477c05586286 -r 43650141d67d src/HOL/ex/InSort.ML
--- 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);
diff -r 477c05586286 -r 43650141d67d src/HOL/ex/Qsort.ML
--- 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