tuned instantiate interface; Logic.incr_tvar;

incr_tvar (from term.ML), incr_indexes: avoid garbage;

added has_duplicates; tuned qsort;

tuned interfaces declare, define, finalize, merge: canonical argument order, produce errors; tuned checkT';

Logic.incr_tvar;

retract accidental user commit; removed obsolete XSYMBOL_HOME; tuned;

tuned;

proving bounds for real linear programs

removed some garbage; fixed record_ex_sel_eq_simproc

textual tweak

Documentation updated

reverted from fold_yield to fold_map

*** empty log message ***

tuned fold on terms and lists;

tuned assoc;

tuned fold on terms; tuned assoc;

tuned min_key, max_key;

replaced foldl_XXX by canonical fold_XXX; canonical arguments for add_term_varnames, add_tvarsT, add_tvars, add_vars, add_frees,

tuned;

tuned fold on terms;

* Pure/library.ML: several combinators for linear functional transformations; * Pure/library.ML: canonical list combinators fold, fold_rev, and fold_yield; * Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types, fold_types;

optimize no_types_needed, remove exception handler

tuned;

lucas - slightly cleaned up. Removed redudent copy of Symtab structure.

* Improved 'oracle' command -- type-safe;

no open Logic;

removed itlist, rev_itlist -- use fold_rev, fold instead; improved end_itlist;

replaced itlist by fold_rev; replaced rev_itlist by fold;

replaced itlist by fold_rev;

use sys_error instead of exception Internal; actually use Termtab; tuned;

sys_error;

type-safe 'oracle' command;

added dest_table;

invoke_oracle: do not keep theory value, but theory_ref;

occs no longer infix (structure not open);

NameSpace.dest_table avoids duplicated extern;

with_path;

removed mk_prodT, mk_not (cf. HOL/hologic.ML); tuned;

tuned;

use all files in HOLCF.thy;

replaced Utils.itlist by fold_rev;

proper structure;

use existing Inttab;

improved oracle setup; replace itlist by fold_rev; replace end_itlist by Utils.end_itlist;

improved oracle setup;

removed not_const -- use Not instead; add mk_not;

HOL.Not; tuned;

HOL.Not;

new type-safe interface; added method example;

removed FOL/ex/IffOracle.ML;

obsolete;

improved 'oracle' command;

tuned;

accomodate change of real_of_XXX;

- fixed bug concerning the renaming of axiom names - introduced new function Defs.fast_overloading_info

added ` combinator

(fix for smlnj)

simplified proof of cont_Iwhen3

avoiding even more garbage

Update PGIP packet handling, fixing unique session identifier.

fixed typos in theorem names

Additions to the Real (and Hyperreal) libraries: RealDef.thy: lemmas relating nats, ints, and reals reversed direction of real_of_int_mult, etc. (now they agree with nat versions) SEQ.thy and Series.thy: various additions RComplete.thy: lemmas involving floor and ceiling introduced natfloor and natceiling Log.thy: various additions

tidied

Add ISABELLE_PID for proof_general.ML

tuned msg;

added print_state_hook; renamed proof'' to actual_proof; tuned;

export previous;

removed ad-hoc atp_hook, cal_atp; removed depth_of; tuned;

Toplevel.actual_proof;

avoid excessive exceptions;

Graph: fast_string_ord;

export eq_brl;

added subtract; improved interface; tuned;

export eq_rrule; improved Net interface;

removed obsolete delta stuff;

open ReconPrelim Recon_Transfer;

open ReconPrelim ReconTranslateProof; removed second copy of exception ASSERTION;

tuned;

use Toplevel.print_state_hook instead of adhoc Proof.atp_hook; added call_atp: bool ref; do 'setmp print_mode []', which is more robust than manual ref manipulation; added subtract_simpset, subtract_claset (supercede delta approximation);

tuned concat_with_and; improved Net interface;

improved Net interface;

* Isar session: The initial use of ROOT.ML is now always timed;

Add acceptedpgipelems message

auto update

generlization of some "nat" theorems

relevance filtering is now optional

tidied

fixed comment-out;

fix

Add management for current working directory

(fix for an accidental commit)

Note about theorem dependencies including themselves.

Fix informtheoryloaded/retracted -> informfileloaded/retracted to match pgip.rnc

(intermediate commit)

(corrected wrong commit)

(intermediate commit)

- added cplex package to HOL/Matrix

avoid some garbage

- use TableFun instead of homebrew binary tree in am_interpreter.ML - add Floats to HOL/Real

- introduce Pure/Tools directory - add compute oracle to Pure/Tools

fold_map -> fold_yield, added transformator combinators, added selector combinator

changed orientation of bind_assoc rule

use qualified names for all constants

added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined

generalized types of monadic operators to class cpo; added match function for UU

added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities) added lemmas to Ring_and_Field.thy (reasoning about signs, fractions, etc.) renamed simplification rules for abs (abs_of_pos, etc.) renamed rules for multiplication and signs (mult_pos_pos, etc.) moved lemmas involving fractions from NatSimprocs.thy added setsum_mono3 to FiniteSet.thy added simplification rules for powers to Parity.thy

experimental code to reduce the amount of type information in blast

tweaked

Added \<module> symbol.

Added "attach" keyword for code generator setup.

Auxiliary functions to be used in generated code are now defined using "attach".

Implemented mechanism for attaching auxiliary code to consts_code and types_code declarations.

small text mod

Fixed some problems with the signal handler.

Improved implementation of Defs.is_overloaded.

Some changes to allow mutually recursive, overloaded functions with same name.

added Davenport reference

moved Davenport citation to Main, removed author list

moved gcd to new GCD.thy

proof needed updating because of arith