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;