minor changes due to primrec defintions for +,-,*
authorpusch
Tue Feb 25 15:12:49 1997 +0100 (1997-02-25)
changeset 2683be7b439baef2
parent 2682 13cdbf95ed92
child 2684 9781d63ef063
minor changes due to primrec defintions for +,-,*
src/HOL/Integ/Integ.ML
     1.1 --- a/src/HOL/Integ/Integ.ML	Tue Feb 25 15:11:56 1997 +0100
     1.2 +++ b/src/HOL/Integ/Integ.ML	Tue Feb 25 15:12:49 1997 +0100
     1.3 @@ -579,12 +579,11 @@
     1.4  by (safe_tac (!claset addSDs [less_eq_Suc_add]));
     1.5  by (rename_tac "k" 1);
     1.6  by (res_inst_tac [("x","k")] exI 1);
     1.7 -by (asm_full_simp_tac (!simpset delsimps [add_Suc, add_Suc_right]
     1.8 -                                addsimps ([add_Suc RS sym] @ add_ac)) 1);
     1.9  (*To cancel x2, rename it to be first!*)
    1.10 -by (rename_tac "a b" 1);
    1.11 +by (rename_tac "a b c" 1);
    1.12 +by (Asm_full_simp_tac 1);
    1.13  by (asm_full_simp_tac (!simpset delsimps [add_Suc_right]
    1.14 -                                addsimps (add_left_cancel::add_ac)) 1);
    1.15 +                                addsimps ([add_Suc_right RS sym] @ add_ac)) 1);
    1.16  qed "zless_eq_zadd_Suc";
    1.17  
    1.18  goalw Integ.thy [zless_def, znegative_def, zdiff_def, znat_def]