removed constant int :: nat => int; int is now an abbreviation for of_nat :: nat => int

thm antiquotations

transaction: context_position (non-destructive only);

added map_current; simplified internal type proof;

tuned msg;

apply_method/end_proof: pass position; Method.Basic: include position;

renamed map to map_current;

tuned;

removed unused is_atomic;

renamed prove_raw to prove_internal; tuned;

merge/merge_refs: plain error instead of exception TERM;

Context positions.

added context_position.ML;

renamed Goal.prove_raw to Goal.prove_internal;

Method.Basic: include position;

tuned proofs: avoid implicit prems;

Basic text: include position; assumption/close: refer to non-atomic assumptions as well, implicit use of prems now considered legacy feature;

thm antiquotations

add lemma inj_of_nat

thm antiquotations

Unfortunately needed patch due to incompatibility with SML -- oo is infix and hence can not appear on the left handside of patterns

changed int stuff into integer for SMLNJ compatibility

more of_rat lemmas

add function of_rat and related lemmas

turned curry (op opr) into curry op opr --- because of smlnj

De-overloaded operations for int and real.

SML basis with type int representing proper integers, not machine words.

Tuned proofs : now use 'algebra ad: ...'

cooper_tac takes now two lists of theorems to be added/deleted from the simpset dor pre-simplification

changed val restriction to local due to smlnj

Changed normalizer Data to contain a simpset besides the list of instances; Before the method starts, it simplifies with this simpset; Added attribute 'algebra' to add and delete theorems from the simpset above;

Added algebra_tac; tuned;

Method now takes theorems to be added or deleted from a simpset for simplificatio before the core method starts

algebra_tac moved to file Tools/Groebner_Basis/groebner.ML; Method now takes theorems to be added or deleted from a simpset for simplificatio *before* the core method starts

nex example

Conversion for computation on constants now depends on the context

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;

Added two examples in Complex/ex :Reflected QE for linear real arith and QE for mixed integer real linear arithmetic

Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers

tuned boostrap

eliminated Code_Generator.thy

tuned integers

tuned;

fixed type int vs. integer;

renamed locale ring/semiring to gb_ring/gb_semiring to avoid clash with Ring_and_Field versions;

add new lemmas

Polynomials now only depend on Deriv; Definition of degree changed

lemma lemma_DERIV_subst moved to Deriv.thy

tuned proofs;