--- a/src/HOL/Lex/AutoChopper.ML Thu Jul 06 15:38:26 2000 +0200
+++ b/src/HOL/Lex/AutoChopper.ML Thu Jul 06 15:38:42 2000 +0200
@@ -11,14 +11,6 @@
Addsimps [Let_def];
-(* Junk: *)
-val [maj,min] = goal Prefix.thy "[| Q([]); !! y ys. Q(y#ys) |] ==> ! l. Q(l)";
-by (rtac allI 1);
-by (induct_tac "l" 1);
-by (rtac maj 1);
-by (rtac min 1);
-val list_cases = result();
-
Goalw [acc_prefix_def] "~acc_prefix A [] s";
by (Simp_tac 1);
qed"acc_prefix_Nil";
@@ -83,7 +75,7 @@
by (res_inst_tac [("p","acc A (start A) ([],list) [] list []")] PairE 1);
by (rename_tac "vss lrst" 1);
by (Asm_simp_tac 1);
-by (res_inst_tac[("xs","vss")] list_eq_cases 1);
+by (case_tac "vss" 1);
by (hyp_subst_tac 1);
by (Simp_tac 1);
by (fast_tac (claset() addSDs [no_acc]) 1);
@@ -214,8 +206,9 @@
by (asm_simp_tac HOL_ss 1);
by (res_inst_tac [("x","x")] exI 1);
by (Asm_simp_tac 1);
- by (rtac list_cases 1);
- by (Simp_tac 1);
+ by(rtac allI 1);
+ by(case_tac "as" 1);
+ by (Asm_simp_tac 1);
by (asm_simp_tac (simpset() addcongs[conj_cong]) 1);
by (strip_tac 1);
by (res_inst_tac [("f","%k. a#k")] ex_special 1);
@@ -225,8 +218,9 @@
by (asm_simp_tac HOL_ss 1);
by (res_inst_tac [("x","x")] exI 1);
by (Asm_simp_tac 1);
- by (rtac list_cases 1);
- by (Simp_tac 1);
+ by(rtac allI 1);
+ by(case_tac "as" 1);
+ by (Asm_simp_tac 1);
by (asm_simp_tac (simpset() addcongs[conj_cong]) 1);
by (Asm_simp_tac 1);
by (strip_tac 1);
@@ -235,8 +229,9 @@
by (subgoal_tac "r @ [a] ~= []" 1);
by (Fast_tac 1);
by (Simp_tac 1);
-by (rtac list_cases 1);
- by (Simp_tac 1);
+by(rtac allI 1);
+by(case_tac "as" 1);
+ by (Asm_simp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [acc_prefix_def] addcongs[conj_cong]) 1);
by (etac thin_rl 1); (* speed up *)
by (Fast_tac 1);