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;