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;

tuned warning msg;

major cleanup; removed several obsolete functions; moved file stuff to Thy/file.ML;

moved 'latex' from library.ML to goals.ML;

tuned prths;

structure BasisLibrary;

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

renamed split_prem_tac to split_asm_tac

restored last version

simpdata.ML: renamed split_prem_tac to split_asm_tac, added split_if_asm cladata.ML: unintentinally committed

renamed split_T_case_prem to split_T_case_asm

renamed split_prem_tac to split_asm_tac

renamed split_prem_tac to split_asm_tac split_asm_tac: simplification, debugged first_prem_is_disj

Fixed indentation

Rationalized the theorem if_image_distrib. Added parens to not_empty.

Fixed indentation

Fixed spelling error

Made some proofs more robust

Now applies "map negOfGoal" to lits when expanding haz rules. Also improved comments

ASCII-fied;

polished definition of find_index_eq

check files for non-ASCII characters;

replaced 8bit characters

fixed LAM<...> syntax;

fixed spelling;

added split_prem_tac

changed libraray function find to find_index_eq, currying it

added contrapos

added contrapos2

added exists_Const

Each datatype t now proves a theorem split_t_case_prem P(t_case f1 ... fn x) = (~((? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1)) | ... (? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn)) ) )

Perl no longer optional;

deriv: eliminated references to theory;

tuned;

tuned;

hyp_subst_tac checks if the equality has type variables and uses a suitable method if so. Affects the dest_eq function

subgoal_tac displays a warning if the new subgoal has type variables

mkdir -p bin;

Tools/8bit: ./mk;

*** empty log message ***

tuned;

abandoned generation of tmp files

various improvements

reflecting changes of isa2latex

several minor improvements

added ax2isa

added ax2isa

added isabelle14 and isabelle24

removed gererated files

added entry for manual

*** empty log message ***

Now introduces Safe_tac

Ran expandshort, especially to introduce Safe_tac

Adapted to removal of UN1_I, etc

Adapted to removal of UN1_I, etc

UNIV now a constant; UNION1, INTER1 now translations and no longer have separate rules for themselves

Expandshort; new theorem le_square

generalized UNION1 to UNION

Tidied Key_supply3

fixed comment

UNIV & UNION1

Ran expandshort, especially to introduce Safe_tac

Ran expandshort, especially to introduce Safe_tac

adapted typed_print_translation;

tuned record_info;

fixed exception OPTION;

adapted pure_trfunsT; added type_tr/tr'; eliminated mk_ofclassS_tr';

print translation: added show_sorts argument;

adapted syn_ext_trfunsT;

adapted extend_trfunsT;

fixed exception OPTION;

added TYPE syntax; tuned;

fixed exception OPTION;

adapted add_trfunsT; defs: admit TYPE arguments;

adapted add_trfunsT;

fixed exception OPTION; added try, can;

base root = "";

Added an alternativ version of AutoChopper and a theory for the conversion of automata into regular sets.

removed redundant ball_image added image_cong and not_empty added ball and bex of UNIV

removed redundant ball_empty and bex_empty (see equalities.ML)

added several theorems

added the, option_map, and case analysis theorems

added zip and nodup

added theorems for Eps