check_overloading replaces datatype overloading; tuned;

added add_tfreesT, add_tfrees; added bound; added zero_var_indexesT, zero_var_indexes, zero_var_indexes_subst; removed add_term_constsT; tuned;

norm_hhf_rule: Thm.adjust_maxidx_thm before Drule.gen_all; removed prove_standard, prove_multi_standard;

added add_const_constraint(_i), const_constraint; added typ_match, typ_unify;

adapted Type.typ_match; tuned;

Sign.typ_unify; Term.bound; tuned rewrite_term;

Term.bound;

print_theory: const constraints;

Type.raw_instance, Type.raw_unify, Term.zero_var_indexesT;

Sign.typ_match;

Sign.typ_unify;

fixed var index in tactic;

proper header;

Sign.typ_instance;

updated;

tuned;

now for Mailman-enabled mailing list

now for Mailman-enabled mailing list

now for Mailman-enabled mailing list

simpler variable names, and no types for monomorphic constants

removed the dependence on abs_mult

fixed typo

brought ML files up to date with new lemmas

renamed Exh_Ssum1 to Exh_Ssum; cleaned up

cleaned up

removed duplicated code; generate new lub and thelub lemmas for new cpo types

cleaned up; renamed some theorems

add theorem fix_defined_iff; cleaned up

add theorem cpair_defined_iff

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