1.1 --- a/src/HOL/Integ/cooper_proof.ML	Fri Mar 19 11:06:53 2004 +0100
     1.2 +++ b/src/HOL/Integ/cooper_proof.ML	Wed Mar 24 10:50:29 2004 +0100
     1.3 @@ -44,7 +44,7 @@
     1.4  (*-----------------------------------------------------------------*)
     1.5  
     1.6  val presburger_ss = simpset_of (theory "Presburger")
     1.7 -  addsimps [zdiff_def] delsimps [thm"zdiff_def_symmetric"];
     1.8 +  addsimps [diff_int_def] delsimps [thm"diff_int_def_symmetric"];
     1.9  val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;
    1.10  
    1.11  (*Theorems that will be used later for the proofgeneration*)