wenzelm [Wed, 07 Jun 2006 01:51:22 +0200] rev 19803
removed obsolete ML files;
wenzelm [Wed, 07 Jun 2006 01:06:53 +0200] rev 19802
removed obsolete ML files;
wenzelm [Wed, 07 Jun 2006 00:57:14 +0200] rev 19801
removed obsolete ML files;
wenzelm [Tue, 06 Jun 2006 20:47:12 +0200] rev 19800
removed Toplevel.debug;
wenzelm [Tue, 06 Jun 2006 20:42:30 +0200] rev 19799
added zip_options;
wenzelm [Tue, 06 Jun 2006 20:42:28 +0200] rev 19798
tuned;
wenzelm [Tue, 06 Jun 2006 20:42:27 +0200] rev 19797
updated;
wenzelm [Tue, 06 Jun 2006 20:42:25 +0200] rev 19796
quoted "if";
nipkow [Tue, 06 Jun 2006 19:24:05 +0200] rev 19795
added type inference at the end of normalization
nipkow [Tue, 06 Jun 2006 19:16:42 +0200] rev 19794
revised nbe command and examples
paulson [Tue, 06 Jun 2006 17:07:27 +0200] rev 19793
new lemmas concerning finite cardinalities
wenzelm [Tue, 06 Jun 2006 16:07:10 +0200] rev 19792
quoted "if";
haftmann [Tue, 06 Jun 2006 15:02:55 +0200] rev 19791
refined code generation
haftmann [Tue, 06 Jun 2006 15:02:09 +0200] rev 19790
added arbitray setup for codegen 2
haftmann [Tue, 06 Jun 2006 15:01:09 +0200] rev 19789
small fix
haftmann [Tue, 06 Jun 2006 14:57:13 +0200] rev 19788
deleted legacy
haftmann [Tue, 06 Jun 2006 14:56:42 +0200] rev 19787
improved code lemmas
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);