pass explicit target record -- more informative peek operation; removed obsolete hide_abbrev; misc tuning;

more informative TheoryTarget.peek operation;

fork_mixfix: explicit bool argument;

eval_term: moved actual evaluation out of CRITICAL section;

preventing eta-redexes in theorems from causing failure

trying to make it run faster

calling the correct interface

replaced syntax/translations by abbreviation;

updated

dropped local_syntax

tuned

(intermediate quickfix)

removed

added

metis calls

updated

moved class power to theory Power

refined; moved class power to theory Power

consolidated naming conventions for code generator theories

class div inherits from class times

code_include replaces code_moduleprolog

added subclass command

enabled Refute_Examples again;

local_axioms: impose hyps stemming from local consts as well (otherwise the axioms will be more general than expected!);

disabled Refute_Examples temporarily;

local_theory: incorporated consts into axioms; LocalDefs.expand_cterm; tuned;

removed unused/impure quiet_mode; local_theory: incorporated consts into axioms; tuned;

added export_cterm; tuned;

local_theory: incorporated consts into axioms;

replaced Term.equiv_types by Type.similar_types; moved add_axiom/def to more_thm.ML;

replaced Term.equiv_types by Type.similar_types;

dest/cert_def: replaced Pretty.pp by explicit Proof.context;

added elim_implies (more convenient argument order); added unvarify (from drule.ML); added specification primitives: add_axiom, add_def;

removed obsolete flip;

moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML); tuned;

replaced (flip Thm.implies_elim) by Thm.elim_implies;

moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);

usedir: added HOL_USEDIR_OPTIONS;

reconstruction bug fix

tuned;

replaced Sign.add_consts_i by Sign.declare_const;

replaced Sign.add_consts_authentic by Sign.declare_const; tuned;

renamed Syntax.XXX_mode to Syntax.mode_XXX; moved ProofContext.pp to Syntax.pp;

removed obsolete AxClass.params_of_class; tuned;

replaced Sign.add_consts_authentic by Sign.declare_const; replaced read_param by Sign.read_const, which is independent of syntax; added define_class_params (from axclass.ML);

load axclass.ML before Isar; load subclass.ML earlier;

added specify_const;

removed obsolete simple_def;

moved define_class_params to Isar/class.ML; removed obsolete params_of_class, print_axclasses; moved ProofContext.pp to Syntax.pp; misc tuning;

load axclass.ML before Isar;

Theory.specify_const;

moved ProofContext.pp to Syntax.pp;

renamed Syntax.XXX_mode to Syntax.mode_XXX;

replaced Sign.add_consts_authentic by Sign.declare_const;

rationalized redundant code

usage: HOL_USEDIR_OPTIONS;

failure messages

'notation': allow structmixfix;

update_modesyntax: may delete 'structure' notation as well;

'notation': allow 'structure' as well;

removed redundant strip_vars/abs_eqn, use improved Drule.abs_def instead; renamed cert_instantiations to check_instantiations, check input only once (simultaneously!);

replaced add_modesyntax by general update_modesyntax (add or del); tuned;

added 'no_notation';

generalized notation interface (add or del);

tuned;

improved abs_def: only abstract over outermost (unique) Vars;

proper latex antiquotations instead of adhoc escapes;

updated;

added no_notation;

removed dead code

more metis proofs

Prepare proper interface of interpretation_i, interpret_i.

getting rid of type typ_var

tuned;

class: print result is for locale;

context-based treatment of generalization; also handling TFrees in axiom clauses

TheoryTarget.init_cmd;

removed LocalTheory.defs/target_morphism operations; moved target_morphism to local_theory.ML; renamed init_i to init, and init to init_cmd; tuned;

renamed AxClass.get_definition to AxClass.get_info (again); simplified goal setup using Proof.theorem_i;

removed LocalTheory.defs/target_morphism operations; added target_morphism (from theory_target.ML);

AxClass.axiomatize and Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;

removed LocalTheory.defs/target_morphism operations;

renamed AxClass.get_definition to AxClass.get_info (again); tuned intro_classes_tac;

renamed AxClass.get_definition to AxClass.get_info (again); AxClass.axiomatize: renamed XXX_i to XXX, and XXX to XXX_cmd;

renamed AxClass.get_definition to AxClass.get_info (again);

Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;

AxClass.axiomatize: renamed XXX_i to XXX, and XXX to XXX_cmd;

removed LocalTheory.defs, use plain LocalTheory.def;

tuned;

generic Syntax.pretty/string_of operations; added uncheck/unparse_classrel/arity (from sign.ML); tuned;

generic Syntax.pretty/string_of operations; proper installation of unparsers and term_uncheck (contract_abbrevs); removed obsolete pretty/string_of_term/typ/sort/classrel/arity (cf. structure Syntax); tuned;

generic Syntax.pretty/string_of operations; existing pretty_term = Syntax.pretty_term o ProofContext.init etc.; removed pretty_classrel/arity (cf. Syntax/syntax.ML);

generic Syntax.pretty/string_of operations;

updated keywords

moved translation kernel to CodeThingol

tuned

simplified evaluation

integrated FixedPoint into Inductive

added proper subclass concept; improved class target

fixed bug in grobner_ideal

tuned generated comment;

primitive add_def: strip sorts in axiom;

avoid polymorphic equality;

maintain typargs for abbrevs as well;

Codegen.is_instance: raw match, ignore sort constraints; replaced get_axiom by authentic get_axiom_i;

Codegen.is_instance: raw match, ignore sort constraints;

turned keywords invariant/freshness_context into reserved indentifiers;

tuned generated comment;

updated;

moved HOL-Nominal keywords into default collection (isar-keywords.el);

list_codegen and char_codegen now call invoke_tycodegen to ensure that gen_... and term_of_... functions are generated as well.

added first version of user-space type system for class target

clarified

Isar-fied many proofs

changed VC-Compatible to VC_Compatible

changed file name

added the two new examples from Nominal to the build process

added two new example files

modernized specifications;

modernized specifications; removed legacy ML bindings;