2006-06-07 wenzelm 2006-06-07 added facts_of; tuned interfaces;
2006-06-07 wenzelm 2006-06-07 added Tools/invoke.ML;
2006-06-07 wenzelm 2006-06-07 renamed Type.(un)varifyT to Logic.(un)varifyT; made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround;
2006-06-07 wenzelm 2006-06-07 do not open Logic;
2006-06-07 wenzelm 2006-06-07 tuned;
2006-06-07 wenzelm 2006-06-07 removed obsolete ML files;
2006-06-07 wenzelm 2006-06-07 removed obsolete ML files;
2006-06-07 wenzelm 2006-06-07 removed obsolete ML files;
2006-06-06 wenzelm 2006-06-06 removed Toplevel.debug;
2006-06-06 wenzelm 2006-06-06 added zip_options;
2006-06-06 wenzelm 2006-06-06 tuned;
2006-06-06 wenzelm 2006-06-06 updated;
2006-06-06 wenzelm 2006-06-06 quoted "if";
2006-06-06 nipkow 2006-06-06 added type inference at the end of normalization
2006-06-06 nipkow 2006-06-06 revised nbe command and examples
2006-06-06 paulson 2006-06-06 new lemmas concerning finite cardinalities
2006-06-06 wenzelm 2006-06-06 quoted "if";
2006-06-06 haftmann 2006-06-06 refined code generation
2006-06-06 haftmann 2006-06-06 added arbitray setup for codegen 2
2006-06-06 haftmann 2006-06-06 small fix
2006-06-06 haftmann 2006-06-06 deleted legacy
2006-06-06 haftmann 2006-06-06 improved code lemmas
2006-06-06 haftmann 2006-06-06 fixed typo
2006-06-06 haftmann 2006-06-06 bugfixes
2006-06-06 krauss 2006-06-06 HOL/Tools/function_package: Applies CodeGen attributes again, where possible.
2006-06-06 ballarin 2006-06-06 Improved parameter management of locales.
2006-06-06 krauss 2006-06-06 HOL/Tools/function_package: imporoved handling of guards, added an example
2006-06-06 krauss 2006-06-06 HOL/Tools/function_package: More cleanup
2006-06-05 wenzelm 2006-06-05 export read/cert_expr; moved type witness to element.ML (abstract type); tuned;
2006-06-05 wenzelm 2006-06-05 guess: more careful about local polymorphism; guess: explicit term vars in statement (avoids warning);
2006-06-05 wenzelm 2006-06-05 assm_tac: try rule termI;
2006-06-05 wenzelm 2006-06-05 added params_of, prems_of; added type witness (from locale.ML); misc cleanup;
2006-06-05 wenzelm 2006-06-05 added matches_seq (left-to-right matching, intermediate beta-normalization);
2006-06-05 wenzelm 2006-06-05 support embedded terms;
2006-06-05 wenzelm 2006-06-05 allow non-trivial schematic goals (via embedded term vars);
2006-06-05 krauss 2006-06-05 HOL/Tools/fundef_package: Cleanup
2006-06-05 urbanc 2006-06-05 added some further lemmas that deal with permutations and set-operators
2006-06-05 urbanc 2006-06-05 added the lemma perm_diff
2006-06-05 krauss 2006-06-05 HOL/Tools/function_package: Added support for mutual recursive definitions.
2006-06-05 krauss 2006-06-05 Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure". This simplifies some proofs.
2006-06-04 mengj 2006-06-04 ATP/res_clasimpset.ML has been merged into res_atp.ML.
2006-06-04 mengj 2006-06-04 Functions of Tools/ATP/res_clasimpset.ML are now in Tools/res_atp.ML. res_clasimpset.ML is not used anymore.
2006-06-03 paulson 2006-06-03 generalized wfI
2006-06-02 wenzelm 2006-06-02 misc cleanup;
2006-06-02 wenzelm 2006-06-02 removed obsolete ML files;
2006-06-02 wenzelm 2006-06-02 tuned;
2006-06-02 wenzelm 2006-06-02 tuned;
2006-06-02 wenzelm 2006-06-02 removed obsolete ML files;
2006-06-02 wenzelm 2006-06-02 merge: always normalize (and check!) reductions;
2006-06-01 huffman 2006-06-01 removed legacy ML scripts
2006-06-01 wenzelm 2006-06-01 tuned;
2006-06-01 wenzelm 2006-06-01 removed obsolete ML files;
2006-06-01 wenzelm 2006-06-01 lemmas strip;
2006-06-01 wenzelm 2006-06-01 removed obsolete ML files;
2006-06-01 urbanc 2006-06-01 added some installation notes for the nominal package
2006-06-01 paulson 2006-06-01 Tiny code cleanup
2006-06-01 urbanc 2006-06-01 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
2006-06-01 urbanc 2006-06-01 added the hack "reset NameSpace.unique_names" to Nominal.thy (Stefan is working on a real fix in the nominal_package)
2006-05-30 schirmer 2006-05-30 tuned type print-translations ----------------------------------------------------------------------
2006-05-29 wenzelm 2006-05-29 proper meta definition;