ISABELLE_TMP;

Added DiffCancelSums.

New guarantee B_trusts_NS5, and tidying

speed-up

args for record data

Removed "open Mutil;"

Added comments

New timing functions startTiming and endTiming

addsplits now in FOL, ZF too

New example

Printing of statistics including time for search & reconstruction

New example

Removed dead code.

Moved the quantifier elimination simp procs into Provers.

Quantifier elimination procs.

Fixed the definition of `termord': is now antisymmetric.

several minor updates;

SYNC;

removed read_cterms;

fixed warning;

removed same_thm;

Tidying, mostly indentation

Deleted some needless addSIs; got rid of a slow Blast_tac

mk_norm_sum;

separate lists of simprocs;

Added rule impCE'

Blast_tac can prove Pelletier\'s problem 46\!

Tidying and using equalityCE instead of the slower equalityE

The change from iffE to iffCE means fewer case splits in most cases. Very few proofs are affected, almost none adversely

Tidying

Tidying and modification to cope with iffCE

Added rule impCE'

Changes to AddIs improve performance of Blast_tac

Statistics

updated comment

Tidying and modification to cope with iffCE

added Suc_mult_less_cancel1, Suc_mult_le_cancel1, Suc_mult_cancel1;

added Arith provers;

Setup various arithmetic proof procedures.

added dest_nat;

moved to Arith/;

Cancel common constant factor from balanced exression.

Cancel common summands of balanced expressions.

removed conv_prover;

tuned;

added crep_cterm;

fixed type of thms_containing;

added foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a; added foldl_aterms: ('a * term -> 'a) -> 'a * term -> 'a; added foldl_types: ('a * typ -> 'a) -> 'a * term -> 'a;

cleaned signature; added instantiate': ctyp option list -> cterm option list -> thm -> thm;

removed merge_opts;

managed merge details;

resolved merge conflict;

Added read_def_cterms for simultaneous reading/typing of terms under defaults. Redefined read_def_cterm in in terms of read_def_cterms. Deleted obsolete read_cterms. Cleaned up def of read_insts, which is not much shorter but much clearere are correcter now.

fixed warning;

made SML/NJ happy;

tuned;

replaced by seq.ML;

changed Pure/Sequence interface;

SYNC;

cd, use: path variables;

comment;

obsolete;

changed Pure/Sequence interface -- isatool fixseq;

changed Sequence interface (now Seq, in seq.ML);

cd, use etc. now support path variables; changed Pure/Sequence interface;

fix references to obsolete Pure/Sequence structure;

tidying

analz_mono_contra_tac was wrong

Deleted some useless comments

minor improvements of formulation and proofs

corrected INDUCT_FILES

$ISABELLE_HOME/src;

improved error msg;

removed old note;

adapted print methods;

improved theorems print method: transfer_sg;

init_data: improved print method;

removed data.ML (made part of sign.ML);

added type object = exn;

added transfer_sg;

fixed xstr token encoding;

tuned infer_types interface;

tuned infer_types interface;

moved Sign.print_sg to display.ML;

exported pretty_classrel, pretty_arity; added infer_types_simult; tuned infer_types interface; moved print_sg to display.ML;

added get_error: 'a error -> string option, get_ok: 'a error -> 'a option; added multiply: 'a list * 'a list list -> 'a list list;

added implode_xstr: string list -> string, explode_xstr: string -> string list;

Now uses induct_tac

Updated the NatSum example

New, higher-level definition of \\out macro

Speeded up the proof of succ_lt_induct_lemma

Two new rewrites

Got rid of some slow deepen_tac calls

Renamed "overload" to "overloaded" for sml/nj compatibility

No more makeatletter/other

Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys

The dtac was discarding information, though apparently no proofs were hurt

Fixed bug in inst_split.

improved big_rec_name lookup;

Updated comments. A bug causes MLWorks to use much more storage than necessary

Rationalized error handling: if low-level tactic (depth_tac) cannot accept the goal then it raises exception TRANS. Top-level tactics (blast_tac) generate warnings and then fail immediately.

Tuned function mk_cntxt_splitthm. Fixed bug which caused split_tac to fail when (Const ("splitconst", ...) $ ...) was of function type.

Removed "(ALL x:f``A. P x) = (ALL x:A. P(f x))", "(EX x:f``A. P x) = (EX x:A. P(f x))", again, because they were already there and added "(UN x:f``A. B x) = (UN a:A. B(f a))" "(INT x:f``A. B x) = (INT a:A. B(f a))" instead.

Redesigned the decision procedures for (Abelian) groups and commutative rings.

Added > "(? x : f `` A. P x) = (? a:A. P(f a))" > "(! x : f `` A. P x) = (! a:A. P(f a))"

merge_refs: check for different versions of theories;

export read_raw_typ;

fixed record parser;

improved record syntax;

made SML/NJ happy;

added thin_refl to hyp_subst_tac

refer to $ISABELLE_HOME/src;

structure BasisLibrary;

renamed to use.ML;

Redefine 'use' command in order to support path variable expansion, automatic suffix generation, and symbolic input filtering (if required).

adapted to new Use, File structs;

added path variables;

File system operations.

moved old file stuff from library.ML to Thy/browser_info.ML; subdir_of no longer infix;

added file.ML, use.ML; removed symbol_input.ML;