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