renamed ProofContext.fix_frees to Variable.fix_frees;

replaced ProofContext.extern_skolem by slightly more simplistic ProofContext.revert_skolems;

no_vars: based on Variable.import; tuned;

added fix_frees (from Isar/proof_context.ML);

declare_term_names: cover types as well; removed unused zero_var_indexesT; tuned;

eliminated obsolete freeze_thaw;

type annotation added to make SML/NJ happy

"moved basic assumption operations from structure ProofContext to Assumption;"

ProofContext.legacy_pretty_thm;

added legacy_pretty_thm (with fall-back on ProtoPure.thy); moved basic assumption operations to assumption.ML; tuned;

Assumption.assume; moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);

removed obsolete is_fact (cf. Thm.no_prems);

tuned interfaces; moved basic assumption operations from structure ProofContext to Assumption;

read_def_cterms (legacy version): Consts.certify;

Assumption.assume;

moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);

removed obsolete equal_abs_elim(_list);

removed obsolete pretty_thm_no_quote;

added Pure/assumption.ML;

moved basic assumption operations from structure ProofContext to Assumption;

tuned proofs;

Local assumptions, parameterized by export rules.

updated;

import(T): result includes fixed types/terms; focus: tuned interface;

focus: result record includes (fixed) schematic variables; SUBGOAL: disallow pending subgoals, more robust re-composition;

Variable.import(T): result includes fixed types/terms;

linear arithmetic splits certain operators (e.g. min, max, abs)

added eval_term

updated;

fixed LaTeX problem;