changed typed_print_translation;

tuned;

nat_cancel enabled by default;

adapted proofs to cope with simprocs nat_cancel;

improved arbitrary_def: we now really don't know nothing about it!

use_thy no longer requires writable current directory;

adapted proofs to cope with simprocs nat_cancel (by Stefan Berghofer);

simplification procedures nat_cancel enabled by default;

tmp_name;

added print_simpset;

added is_base;

added reset_context;

added eq_set;

moved global_names ref to Pure/ROOT.ML;

pred -> -1

pred n -> n-1

Simplified proofs.

Added thm mult_div_cancel

n ~= 0 should become 0 < n

Replaced n ~= 0 by 0 < n

pass return code!!

Fixed the treatment of substitution for equations, restricting occurrences of variables on the RHS. Improves performance in many cases, though a few old proofs fail

updated for latest Blast_tac, which treats equality differently

Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML

Tidying and some comments

updated for latest Blast_tac, which treats equality differently

Instantiated the one-point-rule quantifier simpprocs for FOL New file fologic.ML holds abstract syntax operations Also, miniscoping provided for intuitionistic logic

updated for latest Blast_tac, which fixes an equality bug

Miniscoping now used except for one proof

adapted to new term order;

tuned term order; added indexname_ord, typ_ord, typs_ord, term_ord, terms_ord;

tuned trfuns types;

added prod_ord, dict_ord, list_ord;

File.tmp_name;

added tmp_name;

ISABELLE_TMP;

added context.ML;

Global contexts: session and theory.

added Thy/context.ML;

open;

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