haftmann [Tue, 06 Jun 2006 14:55:56 +0200] rev 19786
fixed typo
haftmann [Tue, 06 Jun 2006 14:55:19 +0200] rev 19785
bugfixes
krauss [Tue, 06 Jun 2006 11:58:10 +0200] rev 19784
HOL/Tools/function_package: Applies CodeGen attributes again, where possible.
ballarin [Tue, 06 Jun 2006 10:05:57 +0200] rev 19783
Improved parameter management of locales.
krauss [Tue, 06 Jun 2006 09:28:24 +0200] rev 19782
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss [Tue, 06 Jun 2006 08:21:14 +0200] rev 19781
HOL/Tools/function_package: More cleanup
wenzelm [Mon, 05 Jun 2006 21:54:26 +0200] rev 19780
export read/cert_expr;
moved type witness to element.ML (abstract type);
tuned;
wenzelm [Mon, 05 Jun 2006 21:54:25 +0200] rev 19779
guess: more careful about local polymorphism;
guess: explicit term vars in statement (avoids warning);
wenzelm [Mon, 05 Jun 2006 21:54:24 +0200] rev 19778
assm_tac: try rule termI;
wenzelm [Mon, 05 Jun 2006 21:54:23 +0200] rev 19777
added params_of, prems_of;
added type witness (from locale.ML);
misc cleanup;
wenzelm [Mon, 05 Jun 2006 21:54:22 +0200] rev 19776
added matches_seq (left-to-right matching, intermediate beta-normalization);
wenzelm [Mon, 05 Jun 2006 21:54:21 +0200] rev 19775
support embedded terms;
wenzelm [Mon, 05 Jun 2006 21:54:20 +0200] rev 19774
allow non-trivial schematic goals (via embedded term vars);
krauss [Mon, 05 Jun 2006 19:54:12 +0200] rev 19773
HOL/Tools/fundef_package: Cleanup
urbanc [Mon, 05 Jun 2006 19:09:40 +0200] rev 19772
added some further lemmas that deal with permutations and set-operators