nat_cancel simprocs;

ISABELLE_TMP_PREFIX;

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