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"

fixed goal_XXX;

adapted to qualified names;

adapted to qualified names;

tuned; adapted to qualified names;

adapted to qualified names;

lookup long names of types;

tuned qualified names;

adapted to qualified names;

qualified names;

local;

Sign.base_name;

fixed types of add_XXX; tuned;

fixed types of add_XXX; added base_name; tuned exports; tuned output of sg;

tuned output;

adapted to qualified names;

Sign.base_name;

fixed types of add_XXX;

local;

local section; improved global, local;

addsplits