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;