# HG changeset patch
# User paulson
# Date 908269708 -7200
# Node ID 5266f09db46cabd804c88f23e4aa0fda642dd8e8
# Parent  4a59d99b5ca3e378806e01ddc05d6a97d8a6ace1
length_Suc_conv is no longer given to AddIffs

diff -r 4a59d99b5ca3 -r 5266f09db46c src/HOL/List.ML
--- a/src/HOL/List.ML	Tue Oct 13 11:05:34 1998 +0200
+++ b/src/HOL/List.ML	Tue Oct 13 11:08:28 1998 +0200
@@ -115,7 +115,6 @@
 by (induct_tac "xs" 1);
 by (Auto_tac);
 qed "length_Suc_conv";
-AddIffs [length_Suc_conv];
 
 (** @ - append **)
 
@@ -162,13 +161,10 @@
  by (rtac allI 1);
  by (exhaust_tac "ys" 1);
   by (Asm_simp_tac 1);
- by (fast_tac (claset() addIs [less_add_Suc2] addss simpset()
-                      addEs [less_not_refl2 RSN (2,rev_notE)]) 1);
+ by (Force_tac 1);
 by (rtac allI 1);
 by (exhaust_tac "ys" 1);
-by (fast_tac (claset() addIs [less_add_Suc2] 
-		       addss (simpset() delsimps [length_Suc_conv])
-                       addEs [(less_not_refl3) RSN (2,rev_notE)]) 1);
+by (Force_tac 1);
 by (Asm_simp_tac 1);
 qed_spec_mp "append_eq_append_conv";
 Addsimps [append_eq_append_conv];
@@ -991,15 +987,15 @@
 by (induct_tac "n" 1);
  by (Simp_tac 1);
  by (Blast_tac 1);
-by (asm_full_simp_tac (simpset() delsimps [length_Suc_conv] 
+by (asm_full_simp_tac (simpset() 
 				addsimps [lex_prod_def]) 1);
-by (auto_tac (claset(), simpset() delsimps [length_Suc_conv]));
+by (auto_tac (claset(), simpset()));
   by (Blast_tac 1);
  by (rename_tac "a xys x xs' y ys'" 1);
  by (res_inst_tac [("x","a#xys")] exI 1);
  by (Simp_tac 1);
 by (exhaust_tac "xys" 1);
- by (ALLGOALS (asm_full_simp_tac (simpset() delsimps [length_Suc_conv])));
+ by (ALLGOALS (asm_full_simp_tac (simpset())));
 by (Blast_tac 1);
 qed "lexn_conv";
 
@@ -1007,7 +1003,7 @@
  "lex r = \
 \ {(xs,ys). length xs = length ys & \
 \           (? xys x y xs' ys'. xs= xys @ x#xs' & ys= xys @ y#ys' & (x,y):r)}";
-by (force_tac (claset(), simpset() delsimps [length_Suc_conv] addsimps [lexn_conv]) 1);
+by (force_tac (claset(), simpset() addsimps [lexn_conv]) 1);
 qed "lex_conv";
 
 Goalw [lexico_def] "wf r ==> wf(lexico r)";