ex/qsort.ML

--- a/ex/qsort.ML	Tue Mar 22 08:25:30 1994 +0100
+++ b/ex/qsort.ML	Tue Mar 22 08:26:25 1994 +0100
@@ -6,8 +6,8 @@
 Two verifications of Quicksort
 *)
 
-val ss = sorting_ss addsimps [Qsort.qsort_Nil,Qsort.qsort_Cons];
-
+val ss = sorting_ss addsimps [Qsort.qsort_Nil,Qsort.qsort_Cons]
+                    delsimps [conj_assoc] addsimps conj_ac;
 
 goal Qsort.thy "!x. mset(qsort(le,xs),x) = mset(xs,x)";
 by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
@@ -24,21 +24,15 @@
  "((Alls x:xs.P(x)) & (Alls x:xs.Q(x))) = (Alls x:xs. P(x)&Q(x))";
 by(list_ind_tac "xs" 1);
 by(ALLGOALS(asm_simp_tac ss));
-by(fast_tac HOL_cs 1);
 val ss = ss addsimps [result()];
 
-goal Qsort.thy "(list_all(p,xs) & Q & list_all(q,ys)) = \
-\               (Q & list_all(p,xs) & list_all(q,ys))";
-by(fast_tac HOL_cs 1);
-val lemma1 = result();
-
 goal HOL.thy "((~P --> Q) & (P --> Q)) = Q";
 by(fast_tac HOL_cs 1);
-val lemma2 = result();
+val lemma = result();
 
 goal Qsort.thy "(Alls x:qsort(le,xs).P(x))  =  (Alls x:xs.P(x))";
 by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
-by(ALLGOALS(asm_simp_tac (ss addsimps [lemma1,lemma2])));
+by(ALLGOALS(asm_simp_tac (ss addsimps [lemma])));
 val ss = ss addsimps [result()];
 
 goal Qsort.thy
@@ -46,7 +40,6 @@
 \                     (Alls x:xs. Alls y:ys. le(x,y)))";
 by(list_ind_tac "xs" 1);
 by(ALLGOALS(asm_simp_tac ss));
-by(fast_tac HOL_cs 1);
 val ss = ss addsimps [result()];
 
 goal Qsort.thy