write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks

replaced calls to PropLogic.auxcnf by PropLogic.defcnf again

comment modified

write_dimacs_sat_file writes outer parentheses again

replaced calls to PropLogic.defcnf by PropLogic.auxcnf

minor parameter changes

defcnf renamed to auxcnf, new defcnf algorithm added, simplify added

Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy

defcnf modified to internally use a reference

dead code removal

reformatting and tidying

tidied up the tracing output

streamlined the tptp output

removed unused code

Tuned comment.

Rewrote function remove_suc, since it failed on some equations produced by recdef.

write_dimacs_sat_file now generates slightly smaller files

revised examples

code streamlining

Ressurect seq attribute accidently removed

Sort search results in order of relevance, where relevance = a) better if 0 premises for intro or 1 premise for elim/dest rules b) better if substitution size wrt to current goal is smaller Only applies to intro, dest, elim, and simp (contributed by Rafal Kolanski, NICTA)

Inttab.defined;

some structured proofs on completeness;

more contribs;

tuned;

isatool fixheaders;

with_path;

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;