outer_params: Syntax.dest_internal;

avoid unqualified exception;

added quoting via back quotes

updated IsaMakefiles for new location of IsaPlanner.

removed IsaPlanner - these are now in Provers.

removed IsaPlannner things from Pure. Moved to Provers.

moved to new location in Provers.

added updated version of IsaPlanner and substitution.

unique_names no longer set to false (thanks to improved naming scheme for "internal" constructors).

- Changed naming scheme: names of "internal" constructors now have "_Rep" as suffix - no need to set unique_names to false any longer - Cleaned up a bit (removed occurrences of strip_option and replace_types')

nbe -> NormalForm

CVS: ----------------------------------------------------------------------

renamed command

renamed file

Removed "code del" declarations again.

fixed owner bug

less_equal -> less_eq (someone had screwd up here)

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;