tuned;

generalized proofs so that call graphs can have any node type.

macbroy5: trying -j 2;

tuned conjunction tactics: slightly smaller proof terms;

tuned laws for cancellation in divisions for fields.

moved nonzero_mult_divide_cancel_right to Ring_and_Field as nonzero_mult_divide_cancel_right'; tuned proofs

Added eta_conv and eta-expansion conversion: waiting for it to be in thm.ML; exported is_refl

gen_qelim_conv now reduces the universal quatifier to the existential one; Now also deals with Ex f for eta-contracted f;

thin_prems_tac first max-scopes universal quantifiers; eta_conv moved to Pure/conv.ML

Tuned error messages; tuned;

normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)

added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub

moved lemma all_not_ex to HOL.thy ; tuned proofs

Tuned instantiation of Groebner bases to fields

added Theorem all_not_ex

renamed vars in zle_trans for compatibility

tuned

The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no longer need class numeral_ring. This made a number of special simp-thms redundant.

Locally added definition of "int :: nat => int" again to make code generation work.

made divide_self a simp rule

Removed thunk from Fun

Church numerals added

method assumption: uniform treatment of prems as legacy feature;

tuned proofs;

tuned proofs: avoid implicit prems;

fixed term_constants (impact on is_relevant); terms in generalize_tac are sorted before we abstract over them (to *try* to avoid the case when a term to be abstracted over already occurs in an other)

no computation rules in the pre-simplifiaction set

Added some lemmas to default presburger simpset; tuned proofs

tuned proofs: avoid implicit prems;

tuned proofs: avoid implicit prems; tuned partition proofs;

Now ResHolClause also does first-order problems!

Now also handles FO problems

Deleted unused code

tidied

tuned proofs: avoid implicit prems;

clarified who we consider to be a contributor

Fixed Problem with ML-bindings for thm names;

fixed filter syntax

updated 'find_theorems' -- moved ProofGeneral specifics to ProofGeneral/CHANGES;

tuned proofs: avoid implicit prems;

int abbreviates of_nat

tuned proofs: avoid implicit prems; tuned;

tuned proofs: avoid implicit prems; major cleanup of proofs/document;

tuned comments;

tuned proofs: avoid implicit prems;

clean up instance proofs; reorganize section headings

reactivated theory Class;

added the Q_Unit rule (was missing) and adjusted the proof accordingly

* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account; * Isar: implicit use of prems from the Isar proof context is considered a legacy feature;

generate_fresh works even if there is no free variable in the goal

tuned;

tuned proofs: avoid implicit prems;

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;