src/HOL/Integ/cooper_proof.ML
changeset 14259 79f7d3451b1e
parent 14139 ca3dd7ed5ac5
child 14479 0eca4aabf371
     1.1 --- a/src/HOL/Integ/cooper_proof.ML	Tue Nov 18 09:45:45 2003 +0100
     1.2 +++ b/src/HOL/Integ/cooper_proof.ML	Tue Nov 18 11:01:52 2003 +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 [symmetric zdiff_def];
     1.8 +  addsimps [zdiff_def] delsimps [thm"zdiff_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*)
    1.12 @@ -52,7 +52,7 @@
    1.13  val zdvd_iff_zmod_eq_0 = thm "zdvd_iff_zmod_eq_0";
    1.14  val unity_coeff_ex = thm "unity_coeff_ex";
    1.15  
    1.16 -(* Thorems for proving the adjustment of the coeffitients*)
    1.17 +(* Theorems for proving the adjustment of the coefficients*)
    1.18  
    1.19  val ac_lt_eq =  thm "ac_lt_eq";
    1.20  val ac_eq_eq = thm "ac_eq_eq";
    1.21 @@ -68,7 +68,7 @@
    1.22  val qe_exI = thm "qe_exI";
    1.23  val qe_ALLI = thm "qe_ALLI";
    1.24  
    1.25 -(*Modulo D property for Pminusinf an Plusinf *)
    1.26 +(*Modulo D property for Pminusinf and Plusinf *)
    1.27  val fm_modd_minf = thm "fm_modd_minf";
    1.28  val not_dvd_modd_minf = thm "not_dvd_modd_minf";
    1.29  val dvd_modd_minf = thm "dvd_modd_minf";
    1.30 @@ -77,7 +77,7 @@
    1.31  val not_dvd_modd_pinf = thm "not_dvd_modd_pinf";
    1.32  val dvd_modd_pinf = thm "dvd_modd_pinf";
    1.33  
    1.34 -(* the minusinfinity proprty*)
    1.35 +(* the minusinfinity property*)
    1.36  
    1.37  val fm_eq_minf = thm "fm_eq_minf";
    1.38  val neq_eq_minf = thm "neq_eq_minf";
    1.39 @@ -87,7 +87,7 @@
    1.40  val not_dvd_eq_minf = thm "not_dvd_eq_minf";
    1.41  val dvd_eq_minf = thm "dvd_eq_minf";
    1.42  
    1.43 -(* the Plusinfinity proprty*)
    1.44 +(* the Plusinfinity property*)
    1.45  
    1.46  val fm_eq_pinf = thm "fm_eq_pinf";
    1.47  val neq_eq_pinf = thm "neq_eq_pinf";