tuned setup for the fields instantiation for Groebner Bases;

Added dependency on file Groebner_Basis.thy

Added instantiation of algebra method to fields

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;

Adapted Proofterm.bicompose_proof to Larry's changes in Logic.assum_pairs from 2005-01-24 (revision 1.44).

Method "algebra" solves polynomial equations over (semi)rings

generalize zpower_number_of_{even,odd} lemmas

deleted comments

deleted legacy lemmas

somebody elses problem fixed

filter syntax change

remove redundant lemmas

remove references to preal-specific theorems

define (1::preal); clean up instance declarations

tuned

instance preal :: ordered_cancel_ab_semigroup_add

use new-style class for sq_ord; rename op << to sq_le

take out Class.thy again, because it does not yet compile cleanly

add axclass semiring_char_0 for types where of_nat is injective

changed filter syntax from : to <-

hide filter

tuned list comprehension, changed filter syntax from : to <-

clean up proofs of exp_zero, sin_zero, cos_zero

generalize class constraints on some lemmas

generalize of_nat and related constants to class semiring_1

declare complex_diff as simp rule

New Reflected Presburger added to HOL/ex

Groebner Basis Examples.

print_antiquotations: sort_strings;

tuned document; added Groebner_Examples;

tuned source deps;

simplified/renamed add_numerals;

renamed ex/Eval_Examples.thy;

added ex/Groebner_Examples.thy; renamed ex/Eval_Examples.thy;

tuned document;