Mon, 01 Mar 2010 17:09:42 +0100added type_notation command;
wenzelm [Mon, 01 Mar 2010 17:09:42 +0100] rev 35418
added type_notation command;

Mon, 01 Mar 2010 17:07:36 +0100more uniform treatment of syntax for types vs. consts;
wenzelm [Mon, 01 Mar 2010 17:07:36 +0100] rev 35417
more uniform treatment of syntax for types vs. consts;

Mon, 01 Mar 2010 17:05:57 +0100more recdef (and old primrec) hunting
krauss [Mon, 01 Mar 2010 17:05:57 +0100] rev 35416
more recdef (and old primrec) hunting

Mon, 01 Mar 2010 16:42:45 +0100killed recdefs in HOL-Auth
krauss [Mon, 01 Mar 2010 16:42:45 +0100] rev 35415
killed recdefs in HOL-Auth

Mon, 01 Mar 2010 13:42:31 +0100merged
haftmann [Mon, 01 Mar 2010 13:42:31 +0100] rev 35414
merged

Mon, 01 Mar 2010 13:40:23 +0100replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann [Mon, 01 Mar 2010 13:40:23 +0100] rev 35413
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)

Mon, 01 Mar 2010 12:30:55 +0100export add_quotient_type.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 01 Mar 2010 12:30:55 +0100] rev 35412
export add_quotient_type.

Mon, 01 Mar 2010 09:47:44 +0100made smlnj happy
bulwahn [Mon, 01 Mar 2010 09:47:44 +0100] rev 35411
made smlnj happy

Sun, 28 Feb 2010 23:51:31 +0100more antiquotations;
wenzelm [Sun, 28 Feb 2010 23:51:31 +0100] rev 35410
more antiquotations;

Sun, 28 Feb 2010 22:30:51 +0100more antiquotations;
wenzelm [Sun, 28 Feb 2010 22:30:51 +0100] rev 35409
more antiquotations;
eliminated legacy ML bindings;