disposed Sign.read_typ etc;

renamed is_abbrev_mode to abbrev_mode; added private get_sort (from sign.ML);

ProofContext.abbrev_mode;

moved get_sort to Isar/proof_context.ML; removed obsolete read_def_typ, read_typ, read_typ_syntax, read_typ_abbrev;

tuned signature; removed duplicates of read_typ/cert_typ (cf. RecordPackage.read_typ/cert_typ);

private add_used (from drule.ML); Variable.declare_names;

Variable.declare_typ;

added declare_typ;

moved add_used to Isar/rule_insts.ML;

export read_typ/cert_typ -- version with regular context operations; tuned;

export read_typ/cert_typ -- version with regular context operations;

tuned signature; removed duplicate of RecordPackage.read_typ; replaced Typetab by existing Typtab;

removed duplicate of DatatypePackage.read_typ;

add lemma cfcomp_LAM

add_abbrev: check tfrees of rhs, not tvars (addresses a lapse introduced in 1.65);

slightly tuned

generalized induct_scheme method to prove conditional induction schemes.

add lemma iterate_iterate

* Disposed old term read functions;

replace preorder class with locale

add lemma compact_imp_principal to locale ideal_completion

added type_constraint (formerly in type_infer.ML, which is now loaded later);

TypeExt.type_constraint;

simplified TypeInfer.infer_types;

improved error output -- variant/mark bounds; simplified infer_types -- always freeze, no result substitution;

load type_infer.ML after Syntax module;

eliminated old Sign.read_term/Thm.read_cterm etc.;

moved ProofContext.pretty_proof to ProofSyntax.pretty_proof; read_term: imitate old behaviour (allow_dummies, mode_schematic);

export transfer_syntax; added allow_dummies feature (for legacy emulations); moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;

moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;

removed obsolete term reading operations (cf. old_goals.ML for legacy emulations);

added emulations for simple_read_term/read_term/read_prop (formerly in sign.ML);

removed obsolete read_def_cterms/read_cterm;

load proof term operations later;

more antiquotations;

OldGoals.read_prop;

OldGoals.simple_read_term;

simplified Abel_Cancel setup;

updated generated file;

pervasive cut_inst_tac;

added a progress lemma and tuned some comments

* Rules and tactics that read instantiations now demand a proper context;

added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML); pervasive operations; tuned;

renamed rename_params_tac to rename_tac;

removed obsolete global instantiation tactics (cf. Isar/rule_insts.ML); removed obsolete rename_tac, rename_last_tac; renamed rename_params_tac to rename_tac;

removed obsolete no_qed, quick_and_dirty_prove_goalw_cterm; removed obsolete abbreviations for ML tactic scripts;

removed obsolete global read_insts/read_instantiate (cf. Isar/rule_insts.ML);

inst1_tac: proper context;

pervasive RuleInsts;

updated generated file;

converted ML proofs;

added read_instantiate;

ML tactic: do not abstract over context again;

export eof;

removed obsolete inst;

atomize: proper context; RuleInsts.read_instantiate;

atomize: proper context;

RuleInsts.read_instantiate;

ptac/prolog_tac: proper context;

allE_Nil: only one copy, proven in regular theory source;