Splitting order changed.

added John's example

replaced REPEAT by REPOEAT_DETERM

gmake vs. make

removed obsolete ML files;

removed obsolete ML files;

removed obsolete ML files;

adding case theorems for code generator

slight code generator cleanup

removed 'primitive definitions' added (non)strict generation, minor fixes

fixed typo

* Theory syntax: some popular names (e.g. "class", "if") are now keywords. * Isar: schematic goals are no longer restricted to higher-order patterns. * ML/Pure: Logic.(un)varify only works in a global context, which is now enforced.

Schematic invocation of locale expression in proof context.

added invoke.ML;

added locale_insts;

renamed Type.(un)varifyT to Logic.(un)varifyT; made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround; renaming: removed duplicate, use zip_options;

added 'if' and 'for' keywords; tuned;

added facts_of; tuned interfaces;

added Tools/invoke.ML;

renamed Type.(un)varifyT to Logic.(un)varifyT; made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround;

do not open Logic;

tuned;

removed obsolete ML files;

removed obsolete ML files;

removed obsolete ML files;

removed Toplevel.debug;

added zip_options;

tuned;

updated;

quoted "if";

added type inference at the end of normalization

revised nbe command and examples

new lemmas concerning finite cardinalities

quoted "if";

refined code generation

added arbitray setup for codegen 2

small fix

deleted legacy

improved code lemmas

fixed typo

bugfixes

HOL/Tools/function_package: Applies CodeGen attributes again, where possible.

Improved parameter management of locales.

HOL/Tools/function_package: imporoved handling of guards, added an example

HOL/Tools/function_package: More cleanup

export read/cert_expr; moved type witness to element.ML (abstract type); tuned;

guess: more careful about local polymorphism; guess: explicit term vars in statement (avoids warning);

assm_tac: try rule termI;

added params_of, prems_of; added type witness (from locale.ML); misc cleanup;

added matches_seq (left-to-right matching, intermediate beta-normalization);

support embedded terms;

allow non-trivial schematic goals (via embedded term vars);

HOL/Tools/fundef_package: Cleanup

added some further lemmas that deal with permutations and set-operators

added the lemma perm_diff

HOL/Tools/function_package: Added support for mutual recursive definitions.

Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure". This simplifies some proofs.

ATP/res_clasimpset.ML has been merged into res_atp.ML.

Functions of Tools/ATP/res_clasimpset.ML are now in Tools/res_atp.ML. res_clasimpset.ML is not used anymore.

generalized wfI

misc cleanup;

removed obsolete ML files;

tuned;

tuned;

removed obsolete ML files;

merge: always normalize (and check!) reductions;

removed legacy ML scripts

tuned;

removed obsolete ML files;

lemmas strip;

removed obsolete ML files;

added some installation notes for the nominal package

Tiny code cleanup

added an example suggested by D. Wang on the PoplMark-mailing list; it shows how the height of an alpha-equated lambda term interacts with capture-avoiding substitution

added the hack "reset NameSpace.unique_names" to Nominal.thy (Stefan is working on a real fix in the nominal_package)

tuned type print-translations ----------------------------------------------------------------------

proper meta definition;

fixed bug in type print translations

tuned;

warnings to debug outputs

warnings to debug outputs; default translation to const-typed

Giving the "--silent" switch to E, to produce less output

fixing a variable-clash bug in rule_by_tactic

removed legacy ML scripts;

removed legacy ML scripts;

removed legacy ML scripts;

removed legacy ML scripts;

removed legacy ML scripts;

tuned;

tuned;

complete_split_rule: all Vars; tuned;

unfold/refold: LocalDefs.meta_rewrite_rule; ObjectLogic.full_atomize_tac; tuned;

removed unused extern_thm;

activate Defines: fix frees;

pretty: do not exterm thm names;

forall_intr_list: do not ignore errors;

separate checks for acyclic/wellformed;

freeze_spec: gensym;

tuned;

axiomatization java_lang;

Changed the DFG format's functions' declaration procedure.

Fixed a bug.

A new "spass" method.

Added in settings used by "spass" method.

Added in SPASS oracle.

HOL problems now have DFG output format.

Changed input interface of dfg_write_file.

Added support for DFG format, used by SPASS.

Helper files in DFG format.

add_datatype_axm: finalize specified consts;

tuned;

tuned;

made smlnj happy;

wellformed: be less ambitious about structural containment; tuned;

Pure: update on overloaded defs;

Extended strong induction rule with additional freshness constraints.

add theorem cfcomp_strict

added add_deps, which actually records dependencies of consts (unlike add_finals); tuned;

tuned;

axiomatize class: Theory.add_deps;