PureThy.add_store_axioms_i;

PureThy.add_store_defs_i, PureThy.add_store_axioms_i;

PureThy.add_store_defs_i;

PureThy.add_store_axioms;

fixed qed;

do not change global_names flag;

restructured -- uses PureThy storage facilities;

added ignored_consts, thms_containing, add_store_axioms(_i), add_store_defs(_i), thms_of; tuned pure thys;

always reload .ML *and* .thy file;

PureThy.add_store_defs, PureThy.add_store_axioms;

added ancestors;

added name_of_thm; improved name_thm: does not overwrite existing name;

add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons, add_term_consts, map_typ, map_term: moved from sign.ML to term.ML;

eq_thm moved to thm.ML; store ProtoPure lemmas;

add_store_axioms_i;

Added finite_UNION/SigmaI.

oops;

renamed put_* to store_*;

flipped global_names default;

do not change global_names flag;

Isa94-2 instead of Isa95;

adapted domain and ax_ops package for name spaces

made SML/NJ happy;

Deleted two needless theorems

internalized some names

corrected two comments

Added goal Set.thy "(Union M = {}) = (! A : M. A = {})"; AddIffs [Union_empty_conv]; Good idea??

oops, swap warnings;

record: tuned output;

ProtoPure.flexpair_def;

ProtoPure.flexpair_def;

merge: default to ProtoPure.thy;

ProtoPure.thy etc.;

tuned names; tuned prep_ext_merge;

self_ref: check_stale; moved pure stuff to pure_thy.ML;

eq_thm (from drule.ML);

added declared: T -> string -> bool; intern / extern;

Pure.thy;

ProtoPure.thy;

tuned; added print_data "theorems";

tuned;

removed add_thms_as_axms;

Init 'theorems' data. The Pure theories.

added pure_thy.ML;

tuned;

Modified comment.

Deleted very odd Delsimps[Collect_False_empty] which made proofs fail!

HOL/Map

Added the new theory Map.

added record section;

Sign.name_of;

Sign.stamp_names_of;

improved typ parser, exported;

tuned;

hide id, stamps; added stamp_names_of, name_of; replaced make_draft by prep_ext; improved print_sg; tuned;

Sign.stamp_names_of;

added sort_wrt;

fixed prune of hidden short names;

tuned;

tuned;