# HG changeset patch
# User nipkow
# Date 962890722 -7200
# Node ID 7eff23d0b38066324c1378a3960c2e2fc7a80275
# Parent  b62d5265b9597b90b1206bb63766d117ca3bcf51
Removed some junk thms.

diff -r b62d5265b959 -r 7eff23d0b380 src/HOL/Lex/AutoChopper.ML
--- 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);