src/HOL/List.ML
changeset 5641 5266f09db46c
parent 5537 c2bd39a2c0ee
child 5644 85fd64148873
     1.1 --- a/src/HOL/List.ML	Tue Oct 13 11:05:34 1998 +0200
     1.2 +++ b/src/HOL/List.ML	Tue Oct 13 11:08:28 1998 +0200
     1.3 @@ -115,7 +115,6 @@
     1.4  by (induct_tac "xs" 1);
     1.5  by (Auto_tac);
     1.6  qed "length_Suc_conv";
     1.7 -AddIffs [length_Suc_conv];
     1.8  
     1.9  (** @ - append **)
    1.10  
    1.11 @@ -162,13 +161,10 @@
    1.12   by (rtac allI 1);
    1.13   by (exhaust_tac "ys" 1);
    1.14    by (Asm_simp_tac 1);
    1.15 - by (fast_tac (claset() addIs [less_add_Suc2] addss simpset()
    1.16 -                      addEs [less_not_refl2 RSN (2,rev_notE)]) 1);
    1.17 + by (Force_tac 1);
    1.18  by (rtac allI 1);
    1.19  by (exhaust_tac "ys" 1);
    1.20 -by (fast_tac (claset() addIs [less_add_Suc2] 
    1.21 -		       addss (simpset() delsimps [length_Suc_conv])
    1.22 -                       addEs [(less_not_refl3) RSN (2,rev_notE)]) 1);
    1.23 +by (Force_tac 1);
    1.24  by (Asm_simp_tac 1);
    1.25  qed_spec_mp "append_eq_append_conv";
    1.26  Addsimps [append_eq_append_conv];
    1.27 @@ -991,15 +987,15 @@
    1.28  by (induct_tac "n" 1);
    1.29   by (Simp_tac 1);
    1.30   by (Blast_tac 1);
    1.31 -by (asm_full_simp_tac (simpset() delsimps [length_Suc_conv] 
    1.32 +by (asm_full_simp_tac (simpset() 
    1.33  				addsimps [lex_prod_def]) 1);
    1.34 -by (auto_tac (claset(), simpset() delsimps [length_Suc_conv]));
    1.35 +by (auto_tac (claset(), simpset()));
    1.36    by (Blast_tac 1);
    1.37   by (rename_tac "a xys x xs' y ys'" 1);
    1.38   by (res_inst_tac [("x","a#xys")] exI 1);
    1.39   by (Simp_tac 1);
    1.40  by (exhaust_tac "xys" 1);
    1.41 - by (ALLGOALS (asm_full_simp_tac (simpset() delsimps [length_Suc_conv])));
    1.42 + by (ALLGOALS (asm_full_simp_tac (simpset())));
    1.43  by (Blast_tac 1);
    1.44  qed "lexn_conv";
    1.45  
    1.46 @@ -1007,7 +1003,7 @@
    1.47   "lex r = \
    1.48  \ {(xs,ys). length xs = length ys & \
    1.49  \           (? xys x y xs' ys'. xs= xys @ x#xs' & ys= xys @ y#ys' & (x,y):r)}";
    1.50 -by (force_tac (claset(), simpset() delsimps [length_Suc_conv] addsimps [lexn_conv]) 1);
    1.51 +by (force_tac (claset(), simpset() addsimps [lexn_conv]) 1);
    1.52  qed "lex_conv";
    1.53  
    1.54  Goalw [lexico_def] "wf r ==> wf(lexico r)";