src/HOL/Tools/Function/function.ML
Sat, 02 Jan 2010 23:18:58 +0100 krauss provide simp and induct rules in Function.info
Sat, 02 Jan 2010 23:18:58 +0100 krauss more official data record Function.info
Tue, 17 Nov 2009 14:51:57 +0100 wenzelm eliminated slightly odd name space grouping -- now managed by Isar toplevel;
Fri, 13 Nov 2009 21:11:15 +0100 wenzelm modernized structure Local_Theory;
Fri, 13 Nov 2009 20:41:29 +0100 wenzelm eliminated slightly odd kind argument of LocalTheory.note(s);
Fri, 13 Nov 2009 17:25:09 +0100 wenzelm eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
Tue, 10 Nov 2009 15:33:35 +0100 wenzelm removed unused Quickcheck_RecFun_Simps;
Thu, 05 Nov 2009 22:08:47 +0100 wenzelm adapted LocalTheory.declaration;
Mon, 02 Nov 2009 22:24:03 +0100 krauss conceal partial rules depending on config flag (i.e. when called via "fun")
Mon, 02 Nov 2009 22:24:00 +0100 krauss conceal "termination" rule, used only by special tools
Sun, 01 Nov 2009 15:44:26 +0100 wenzelm modernized structure Context_Rules;
Sun, 01 Nov 2009 15:24:45 +0100 wenzelm modernized structure Rule_Cases;
Sun, 25 Oct 2009 19:21:34 +0100 wenzelm name space groups are identified by serial, not serial_string;
Sat, 24 Oct 2009 20:47:10 +0200 krauss configuration flag "partials"
Fri, 23 Oct 2009 16:22:10 +0200 krauss function package: more standard names for structures and files
less more (0) tip