eliminated unused simproc identifier;

more canonical names

simplified simproc programming interfaces;

prefer tactics with explicit context;

simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);

clarified context;

clarified context;

Thm.cterm_of and Thm.ctyp_of operate on local context;

clarified signature;

tuned signature -- prefer qualified names;

removed dead code;

simplifier uses proper Proof.context instead of historic type simpset;

tuned exceptions -- avoid composing error messages in low-level situations;

more antiquotations;

inlined antiquotations;

misc tuning and modernization;

simplified/unified Simplifier.mk_solver;

proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way;
tuned;

modernized structure Proof_Context;

more antiquotations;

formerly unnamed infix equality now named HOL.eq

renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;

tuned quotes

use antiquotations for remaining unqualified constants in HOL

tuned;

modernized structure Term_Ord;

removed spurious occurrences of old rep_ss;

normalized some ML type/val aliases;

moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
tuned signature of structure Term;

more antiquotations;

simplified get_thm(s): back to plain name argument;

renamed datatype thmref to Facts.ref, tuned interfaces;

added signatures;
tuned

added Statespace library