--- a/ex/qsort.ML Tue Feb 15 07:55:22 1994 +0100
+++ b/ex/qsort.ML Tue Feb 15 10:05:17 1994 +0100
@@ -84,11 +84,6 @@
Qsort.qsort_Nil,Qsort.qsort_Cons];
-goal List.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))";
-by(list_ind_tac "xs" 1);
-by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if]))));
-val ss = ss addsimps [result()];
-
goal Qsort.thy "x mem qsort(le,xs) = x mem xs";
by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if]))));