moved position.ML, path.ML, file.ML to General;

moved name_space.ML to General/name_space.ML;

moved Thy/path.ML to General/path.ML;

moved Thy/position.ML to General/position.ML;

moved Thy/file.ML to General/file.ML;

new type-safe user interface for theory data;

nonterminals prog;

adapted to new theory data interface;

use type-safe theory data interface;

added theory_data.ML;

Type-safe interface for theory data.

* improved the theory data mechanism to support real encapsulation; main change of the internal interfaces: data kind name (string) replaced by private Object.kind, acting as authorization key;

accomodate tuned version of theory data;

added print_theorems: theory -> unit; added print_theory: theory -> unit; added transaction mechanism as last resort to accomodate non-atomic transformers (please avoid such things); tuned setup;

Object.T;

improved data: secure version using Object.T and Object.kind;

tuned setup; tuned add_attributes: comment; accomodate tuned version of data;

use Object.T and Object.kind; added print_data; improved get_data, put_data: more abstract; add_axioms(_i), add_oracle: made atomic transactions;

removed type object (see object.ML);

tuned print_exn;

print_data moved to theory.ML; print_theory: exclude theorems (no forward reference!);

added THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq; added ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq; added APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq; added EVERY: ('a -> 'a seq) list -> 'a -> 'a seq; added FIRST: ('a -> 'b seq) list -> 'a -> 'b seq; added TRY: ('a -> 'a seq) -> 'a -> 'a seq; added REPEAT: ('a -> 'a seq) -> 'a -> 'a seq;

added object.ML;

added option_map_o_empty added option_map_o_empty and option_map_o_update to simpset()

added split_etas

added split_sum_case_asm

tuned;

tuned msgs;

auto update

fixed ml_prompts;

changed get_single: ('a, 'b) source -> ('a * ('a, 'b) source) option;

tuned dist version;

tuned header;

version under control of Admin/makedist;

README, Pure/ROOT.ML: version set automatically;

version under control of Admin/makedist; ml_prompts;

added ml_prompts;

added mapfilter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source; (map)filter: fixed propagation of prompt;

tuned error msg;

fixed error msgs;

Structure Option now declared in MLWorks

mk_all_imp: no longer creates goals that have beta-redexes

more tracing

Changed require to requires for MLWorks

auto update

made SML/NJ happy;

foldl_map prep_field;

tuned store_theory;

tuned local, global; tuned begin and end theory;

tuned store_theory: theory -> unit;

added get_name, put_name, global_path, local_path, begin_theory, end_theory;

global_names moved to pure_thy.ML;

certify_term: type_check replaces Term.type_of, providing sensible error messages; eliminated mapfilt_atoms (use Term.foldl_aterms);

renamed state_source to source'; removed test;

added recover, source;

added catch: ('a -> 'b) -> 'a -> 'b; tuned source(');

remove seq2, scan (use seq2, foldl_map from library.ML);

added foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list; added seq2: ('a * 'b -> unit) -> 'a list * 'b list -> unit; tuned 'beginning';

Swapped order of params.

changed get_single: ('a, 'b) source -> 'a option * ('a, 'b) source; tuned prompt; Scan.source vs. Scan.source';

source vs. source';

tuned keywords;

added is_stale;

tuned signature; added pretty_theory;

tuned comments;

tuned;

Small mods.

prompt made part of source;

fixed handle_error: cat_lines;

added Thy/position.ML;

added source: string -> (string, string list) Source.source;

Input positions.

added Syntax/source.ML;

added Source module;

Co-algebraic data sources.

Symbol.stopper;

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;

proper thy files;

fixed update syntax;

improved source: state-based; tuned bulk;

added scan_tvar;

added 'space';

Got rid of NAe.delta

HOL/Update

Removed some traces of UNITY

Changed [/] to [:=] and removed actual definition.

New syntax for function update; moved to main HOL directory

misc tuning;

'more' selector; thms: selector_convs, update_convs; tuned;