hid constant "dom"

Removed from CVS, since obselete in the new Presburger Method;

Generated reflected QE procedure for Presburger Arithmetic-- Cooper's Algorithm -- see HOL/ex/Reflected_Presburger.thy

Added more examples

Now only contains generic conversion for quantifier elimination in HOL

A new tactic for Presburger;

tuned

Temporarily added theorems for QE that were in old Presburger.thy ; This will diseappear with the new Ferrante and Rackoff shortly;

tuned tactic

Temporarily use int instead of IntInf.int but Code generator should map HOL's int to ML's IntInf.int --- To be fixed

tuned Proof and Document

tuned Proof

A new and cleaned up Theory for QE. for Presburger arithmetic

Added new files for Presburger (cooper_data.ML, cooper.ML) and deleted old unused ones cooper_dec, cooper_proof, reflected_cooper etc..

explicitely depends on file groebner.ML

Context Data for the new presburger Method

A new simpler and cleaner implementation of proof Synthesis for Presburger Arithmetic --- Cooper's Algorithm

remove references to constant int::nat=>int

simplify int proofs

modify proofs to avoid referring to int::nat=>int

add int_of_nat versions of lemmas about int::nat=>int

add lemma of_nat_power

add int_of_nat versions of lemmas about int::nat=>int

add abbreviation int_of_nat for of_nat::nat=>int; add int_of_nat versions of all lemmas about int::nat=>int; move int lemmas into their own section, preparing to remove

disabled theory "Reflected_Presburger" for smlnj (temporarily);

disabled theories MIR and ReflectedFerrack for smlnj (temporarily);

*** empty log message ***

remove dependencies of proofs on constant int::nat=>int, preparing to remove it

eqtype int -- explicitly encourage overloaded equality; tuned -%; removed obsolete Intt;

simplified type integer;