New command: interpretation in locales.

moved wf_induct_rule from PreList.thy to Wellfounded_Recursion.thy

exported after_qed for arity proofs

added finite(option) to Recdef.thy

added selectors 'classes_of' and 'classes_arities_of'

exported dest_def

added 'the_const_constraint'

(added to repository)

(added to repository)

After_qed takes result argument.

Release of interpretation in locale.

fixed typo in ratadd

added hint for position of aqu options in connection with styles

clarified ML_idf

moved some rat functions to library.ML

added more rat functions

Tuned comment.

new lemma

Added ENTCS 2000 paper by Aleksey Nogin.

New case study: pigeonhole principle.

Added Extraction/Pigeonhole.

added Brian Hufmann's finite instances

Fixed bug in code generator for let and split leading to ill-formed code.

Adapted to new argument format of MinProof constructor.

Adapted to new interface og thms_of_proof / axms_of_proof.

Adapted to new interface of thms_of_proof.

- Tuned handling of oracles - Put arguments of axms_of_proof and thms_of_proof into "canonical order"

mentioned change to exp_ge_add_one_self, new transitivity rules

changes from renaming of exp_ge_add_one_self

renamed exp_ge_add_one_self to exp_ge_add_one_self_aux

renamed exp_ge_add_one_self2 to exp_ge_add_one_self

added extra transitivity rules

added Hyperreal/Ln, replaced Lfp and Gfp by FixedPoint

changed reference to Lfp.lfp to FixedPint.lfp, ditto for gfp

import FixedPoint instead of Gfp

removed Gfp

removed Lfp

combined Lfp and Gfp to FixedPoint

tuned ML_OPTIONS;

export clear_ss;

added unfold_tac (Simplifier.inherit_bounds);

simprocs: Simplifier.inherit_bounds;

tuned;

First version of interpretation in locales. Not yet fully functional.

Turned simp_implies into binary operator.

Added filter lemma

* Pure/Simplifier: improved handling of bound variables;

determine Poly/ML runtime system version

obsolete;

determine Poly/ML's idea of current hardware and operating system type;

tuned;

Thm.full_prop_of;

Compress.term;

removed atless (use term_ord instead); removed (inefficient) insert_aterm; improved bound: nameless, avoid allocating new strings; tuned sort_ord/typ_ord: dict_ord; tuned abstract_over: SAME; tuned add_term_vars/frees: OrdList.insert; removed compress_type/compress_type (cf. compress.ML);

export MataSimplifier.inherit_bounds;

Compress.typ;

Compress.init_data;

nameless Term.bound;

improved bounds: nameless Term.bound, recover names for output;

tuned dict_ord;

replaced atless by term_ord;

chain_history: turned into runtime flag; added monomorphic; removed (inefficient) fast_overloading_info; Compress.typ; tuned;

compression of terms and types by sharing common subtrees;

added compress.ML;

Term.is_bound;

tuned signature;

no eq_commute;

Defs.monomorphic;

Sign.read_term;

more zcong_sym;

simprocs: Simplifier.inherit_bounds;

no eq_sym_conv; tuned;

removed read_cterm; tuned;

tuned msg;

PolyML.Compiler.printInAlphabeticalOrder := false;

polyml: use polyml-platform/version from Isabelle distribution; removed DEFS_CHAIN_HISTORY;

obsolete;

1. changed configuration variables for linear programming (Cplex_tools): LP_SOLVER is either CPLEX or GLPK CPLEX_PATH is the path to the cplex binary GLPK_PATH is the path to the glpk binary The change makes it possible to switch between glpk and cplex at runtime. 2. moved conflicting list theories out of Library.thy into ROOT.ML

added map_filter lemmas

Ordering is now: first by number of assumptions, second by the substitution size. Treat elim/dest rules like erule/drule would: * "elim" is now a subset of "dest" and matches on conclusion of goal and major premise against any premise of goal. Computed substitution size takes both into account. * "dest" no longer has a restriction that limits its conclusion to a var. (contributed by Raf)

addedd ID line

mentioned Ln in NEWS

fixed minor typo in comments

changed import to Ln

added a new theory; properties of ln

P.opt_locale_target;

nameless theorems: better names, flag to omit them

invents theorem names; also patches write_out_clasimp

dead code

new function trim_ends

uniform treatment of variable prefixes

corrected some typos

new droplet

Added flag ResClasimp.use_simpset to allow exclusion of simpset rules from ATP problem files

tuned gen_all, forall_elim_list, implies_intr_list, standard; impose_hyps: use Thm.weaken; zero_var_indexes: use Term.zero_var_indexes_inst; Sign.typ_unify;

Sign.typ_unify; tuned;

Sign.typ_unify; Tactic.prove;

typ_match, unify: canonical argument order; added raw_match, raw_instance; proper implementation of raw_unify;

added weaken, adjust_maxidx_thm;

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

(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;