improved finite scans: more abstract stopper; fixed source: now actually handles finite scans; tuned bulk;

snoc_induct/exhaust -> rev_induct_exhaust.

Cleaned up and simplified etc. snoc_induct/exhaust -> rev_induct_exhaust.

witnesses: lookup stored thms instead of axioms;

added add_axioms_x, add_defs_x;

PureThy.add_typedecls;

Reordred arguments in AutoChopper. Updated README with ref to paper.

extended addsplits and delsplits to handle also split rules for assumptions extended const_of_split_thm, renamed it to split_thm_info

simplifications

disabled (experimental) geometry option

keyboard settings now done by loading Tools/8bit/xemacs/isa_xemacs.emacs

added option_map_o_update

added welcome;

added :-- (dependent pair);

added transform_error, exception ERROR_MESSAGE;

added thms_closure: theory -> xstring -> tthm list option; added add_typedecls: (bstring * string list * mixfix) list -> theory -> theory; |> Theory.add_nonterminals Syntax.pure_nonterms;

adapted to new Scan.fail_with / Scan.!!;

pure_nonterms;

added fail_with and adapted !!;

gen_attr: fixed order of evaluation;

tuned msg;

get_first: ('a -> 'b option) -> 'a list -> 'b option;

HOL/record: now includes concrete syntax for record terms;

added Goal, Goalw;

branching_level = 250;

fixed comment;

Removed duplicate list_length_induct

Reordered a few parameters.

Lex

tuned comment;

Reshuffeling, renaming and a few simple corollaries.

fixed translations;