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;

tuned comments;

Semiring normalization and Groebner Bases.

moved generic algebra modules

updated documentation

fixed broken execption handling

simplified notion of "operational classes"

merged Code_Generator.thy into HOL.thy

added a function partition and a few lemmas

added a few theorems about foldl and set

added lcm, ilcm (lcm for integers) and some lemmas about them;

included Class.thy in the compiling process for Nominal/Examples

remove simp attribute from lemma_STAR theorems

add lemma exp_of_real

tuned list comprehension

tuned;

added is_atomic; removed unused is_all;

added assume_rule_tac;

reverted appnd to append

authentic syntax for List.append

tuned comments

added a few comments to the proofs

removed fixmes

opaque-constraint removed

tuned;

monomorphic equality: let ML work out the details;

added gen_merge_lists/merge_lists/merge_alists (legacy operations from library.ML);

tuned Tactic signature;

removed obsolete Library.seq;

moved flip to library.ML; removed unused dest/unfold/unfold_rev; simplified fold/fold_rev/fold_map;

added CSUBGOAL;

cleaned up signature;

added downto0 (from library.ML);

merge_ss: plain merge of prems;

added flip (from General/basics.ML); renamed gen_submultiset to submultiset; moved downto0 to pattern.ML; moved legacy gen_merge_lists/merge_lists/merge_alists to Isar/locale.ML; moved plural to HOL/Tools/fundef_lib.ML; removed obsolete seq; simplified chop, fold2;

tuned document;

use antiquotations instead of raw TeX code; tuned document;

name_of_fqgar: precise type;

added plural (from Pure/library.ML); removed unused eq_str;

local open FundefLib;

renamed gen_submultiset to submultiset;

HOL-ex: tuned deps;

tuned list comprehension, added lemma

fixed tex error

*** empty log message ***

*** empty log message ***

extended

cosmetic

made SML/NJ happy;

added target/local_abbrev (from proof_context.ML); target_abbrev: demand equal head const (tool compliance);

moved specific target/local_abbrev to theory_target.ML;

"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases. more cleanup.

added "plural : 'a -> 'a -> 'b list -> 'a" for convenient error msg construction

proper handling of Tools;

cosmetic

refute_tac made more deterministic

extended

cosmetic

tracing disabled

additional tracing information

tuned

some tests for arith added

Moved list comprehension into List

MiniSAT mentioned in comment

fixed handling of meta-logic propositions

simplified interfaces, some restructuring

updated

added some bibtex entries

Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)

Added simp-rules: "R O {} = {}" and "{} O R = {}"

rudimenary

tuned

dropped superfluous name bindings

localized

fixed typo

insert: canonical argument order;

simplified/unified list fold;

replace (- 1) with -1

simplify some proofs

tuned headers -- adapted to usual conventions;

moved Compute_Oracle from Pure/Tools to Tools;

proper theory setup for compute oracle (based on CPure); simplified oracle setup;

moved IsaPlanner from Provers to Tools; moved Compute_Oracle from Pure/Tools to Tools;

moved IsaPlanner from Provers to Tools;

made aconvc pervasive;

moved aconvc to more_thm.ML;

tuned ML setup;

decode_term: force qualified name into Const;

proper loading of ML files (in HOL.thy); moved Integ files to canonical place; misc cleanup;

HOL_proofs;

moved Integ files to canonical place;

proper loading of ML files;

removed dead code;

tuned header;

doc: exclude isabelle_isar.pdf;

tuned the proof

introduced symmetric variants of the lemmas for alpha-equivalence

proper loading of ML files; removed obsolete IFOL.thy/FOL.thy values;

removed obsolete IFOL.thy/FOL.thy values;

proper loading of ML files;

tuned header;

tuned oracle setup;

moved HOLCF tools to canonical place;

moved TFL files to canonical place;

moved TFL files to canonical place;

added src/Tools; moved TFL files to canonical place;

fixed title;

Tools: generic tools outside of Pure.

moved Integ files to canonical place;

fixed use_thy "LocalWeakening";

included new example in the compiling process

a theory using locally nameless terms and strong induction principles

tuned the proof

emulate later version of TextIO.inputLine;

reversed SML B library patches;

TextIO.inputLine: use present SML B library version;

tuned USEDIR_OPTIONS; PDF_VIEWER: try to be smart for MacOS (Darwin);

removed HOL4 image, which seldom works;

simplified data setup

instance: always print sorts on failure

more example

fixed typo

updated

generalized lemmas

eliminated strings

tuned

clarified error message

simplify names of locale interpretations

renamed some lemmas in Complex.thy