added list of theorem changes to NEWS added real_of_int_abs to RealDef.thy

added defined;

simplified union;

tuned match, unify;

tuned instantiate (avoid subst_atomic, subst_atomic_types); Logic.incr_tvar;

tuned defs interface;

moved incr_tvar to logic.ML; added eq_var, eq_tvar, instantiate, instantiateT;

tuned norm_sort, mg_domain;

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;