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;

added nth_drop

tuned datatype_codegen setup

certificates for code generator case expressions

added illustrative diagnostics

clarified declarations in class ord

concept for exceptions

clarified name suffix

step towards proper purge operation

put declarations first

clarified terminology

intermediate cleanup

clarified relationship of code generator conversions and evaluations

abs_conv/forall_conv: proper context (avoid gensym); removed unused cache_conv;

load variable.ML before conv.ML;

Conv.forall_conv: proper context;

cover AFP logs as well, using "afp" pseudo-platform;

moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;

avoid gensym;

updated Sign.add_abbrev;

combinator translation

avoid unnamed infixes;

avoid unnamed infixes; tuned;

avoid unnamed infixes;

modernized specifications; tuned proofs;

mark inductive results as internal;

skolem_cache: ignore internal theorems -- major speedup; skolem_cache_theorems_of: efficient folding of table; replaced get_axiom by Thm.get_axiom_i (avoids name space fishing);

major speedup by avoiding metis;

modernized definitions;

added add_defs_new, which strips sorts for axioms (presently inactive);

removed unused add_defss;

tuned internal inductive interface;

tuned internal interfaces: flags record, added kind for results; tuned;

inductive: mark internal theorems as Thm.internalK;

tuned;

export tsig_of;

clarified role of class relations

ignore mutual recursive modules

integer compatibility: added wrapper for structure Time;

fixed use_text;

downgraded IntInf with divMod; fixed use_text;

added auto-quickcheck-time-limit;

auto_quickcheck: pervasive options, turned time_limit into plain int, simplified exception handling;

added auto_quickcheck feature;