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;

deriv_tac/DERIV_tac: proper context;

sum3_instantiate: proper context;

eliminated OldGoals.inst;

updated generated file;

method "tactic": only "facts" as bound value; added method "raw_tactic";

Export a wrapper for all semiring_normalizers

proper context for tactics derived from res_inst_tac;

added ~: and ~=; fixed SOME, which is now \<some> not \<epsilon>;

export subgoal_tac, subgoals_tac, thin_tac;

prove: full Variable.declare_term, including constraints;

prove_standard: more precises argument passing; proper context for tactics derived from res_inst_tac;

InductTacs.case_tac: removed obsolete declare, which is now part of Goal.prove;

simplified InductTacs.case_tac/induct_tac;

tuned proof;

removed obsolete nat_induct_tac -- cannot work without;

removed obsolete case_split_tac -- cannot work without;

removed unused excluded_middle_tac; proper context for tactics derived from res_inst_tac; tuned setup;

updated geenrated file;

qualified old res_inst_tac variants;

proper context for tactics derived from res_inst_tac;

updated generated file;

obsolete;

certify_term: reject qualified frees;

removed experimental Poplog/PML support; removed obsolete ML_SUFFIX; some reformatting;

removed obsolete ML_SUFFIX; some reformatting;

removed experimental Poplog/PML support;

removed obsolete ML_SUFFIX;

removed exotic 'token_translation' command;

proper name for LinearQuantifierElim;

removed old theorem database;

map_const: soft version, no failure here (recovers hiding of consts, because a hidden name is illegal and rejected later);

hide: delete all accesses from extra names -- reduces ambiguity in extern;

map_const: soft version, no failure here;

skolem_fact/thm: uniform numbering, even for singleton list; declare_skofuns: eliminated recovery via Clausify_failure -- should be sufficiently robust as is;

hide (open);

no_notation instead of hide;

* Recovered hiding of consts;

updated generated file;

back to CodeTarget.code_width;

hide -> hide (open)

use regular error function;

add lemma finite_image_approx; remove unnecessary sort annotations

change orientation of fix_eqI and convert to rule_format; add lemma fix_ind2

export just one setup function; more antiquotations; to_nnf: import open, avoiding internal variables (bounds); ThmCache: added table of seen fact names; reorganized skolem_thm/skolem_fact/saturate_skolem_cache: maintain seen fact names, ensure idempotent operation for Theory.at_end; removed obsolete skolem attribute (NB: official fact name unavailable here);

removed obsolete skolem declarations -- done by Theory.at_end;

tuned setup;

remove unnecessary import of Ffun; add lemma admD2

imports Ffun

ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context; eliminated obscure theory merge/transfer -- use explicit theory context instead;

ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;

sane versions of (qualified_)thms_of_thy;

Facts.dest/export_static: content difference; tuned;

dest/export_static: content difference; tuned comments;

declare_skofuns/skolem: canonical argument order; minor tuning;

Facts.dest/export_static: content difference;

correction

tuned