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