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;

replaced some 'translations' by 'abbreviation';

* Basic Isabelle mode for jEdit.

tuned generated comment;

tuned;

Basic Isabelle mode for jEdit -- http://www.jedit.org/

isabelle mode for jEdit;

added target tool specification; added jEdit output;

added target tool specification; no special treatment of Pure session;

emacs vs. jedit;

some updates;

removed obsolete write_keywords;

Dummy session with outer syntax keyword initialization.

added Pure-ProofGeneral target (dummy session with outer syntax keyword initialization);

tuned;

use isatool keywords -- generate from logs instead of session images;

removed duplicate target;

updated;

generate outer syntax keyword files from session logs;

export init_outer_syntax;

tuned;

report on keyword/command declarations; tuned;

tuned;

added keyword_decl, command_decl;

added class_expr; tuned;

simplified interfaces for outer syntax; tuned;

simplified interfaces for outer syntax;

updated;

(co)induct: polymorhic taking'';

added burrow_options;

tuned proofs (via polymorphic taking'');

export get_consumes;

tuned Induct interface: prefer pred'' over set'';

coinduct: instantiation refers to suffix of main prop (major premise or conclusion); tuned;

tuned induct etc.;

execute/system: non-critical;

subtract: minor performance tuning;

cover only .gz files;

metis method: used theorems

filtering out some package theorems

added lemmas

single-threaded profiling;

tuned;

Name.uu, Name.aT;

added uu, aT;

replaced literal 'a by Name.aT;

replaced AxClass.param_tyvarname by Name.aT;