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;

certify: check_stale;

improved handling of draft signatures / theories; draft thms (and ctyps, cterms) are automatically promoted to real ones;

sg_ref: automatic adjustment of thms of draft theories;

commit;

made Poly/ML happy, but SML/NJ unhappy;

typo

Corrected alphabetical order of entries in signature.

Fixed the index entries for "recursion, general"

Many minor speedups: 1. Some use of rewriting with expand_ifs instead of addsplits[expand_if] 2. Faster proof of new_keys_not_used 3. New version of shrK_neq (no longer refers to "range")

New rewrite rules image_iff

Documented `addsplits'

make SML/NJ happy;

rm IOA TLA;

tuned types;

tuned sig;

reset global_names;

set global_names;

replaced ops by consts;

removed Dlist;

\label{simp-chap} -> chap:simplification Indexed "higher-order pattern"