# HG changeset patch
# User pusch
# Date 856879969 -3600
# Node ID be7b439baef24d5a92cc8b12bc19ca2a3003d299
# Parent  13cdbf95ed92797a408c15be7308f2eba08f3b30
minor changes due to primrec defintions for +,-,*

diff -r 13cdbf95ed92 -r be7b439baef2 src/HOL/Integ/Integ.ML
--- a/src/HOL/Integ/Integ.ML	Tue Feb 25 15:11:56 1997 +0100
+++ b/src/HOL/Integ/Integ.ML	Tue Feb 25 15:12:49 1997 +0100
@@ -579,12 +579,11 @@
 by (safe_tac (!claset addSDs [less_eq_Suc_add]));
 by (rename_tac "k" 1);
 by (res_inst_tac [("x","k")] exI 1);
-by (asm_full_simp_tac (!simpset delsimps [add_Suc, add_Suc_right]
-                                addsimps ([add_Suc RS sym] @ add_ac)) 1);
 (*To cancel x2, rename it to be first!*)
-by (rename_tac "a b" 1);
+by (rename_tac "a b c" 1);
+by (Asm_full_simp_tac 1);
 by (asm_full_simp_tac (!simpset delsimps [add_Suc_right]
-                                addsimps (add_left_cancel::add_ac)) 1);
+                                addsimps ([add_Suc_right RS sym] @ add_ac)) 1);
 qed "zless_eq_zadd_Suc";
 
 goalw Integ.thy [zless_def, znegative_def, zdiff_def, znat_def]