src/ZF/Datatype.ML
Fri, 16 Dec 1994 17:46:02 +0100 lcp Defines ZF theory sections (inductive, datatype) at the start/
Thu, 24 Nov 1994 00:31:41 +0100 lcp ZF/Datatype/datatype_decl: supplies a SINGLE domain for the mutually
Fri, 12 Aug 1994 12:51:34 +0200 lcp installation of new inductive/datatype sections
Fri, 15 Jul 1994 13:34:31 +0200 clasohm added thy_name to Datatype_Fun's parameter
Mon, 15 Nov 1993 14:41:25 +0100 lcp changed all co- and co_ to co
Fri, 22 Oct 1993 11:34:41 +0100 lcp ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works
Fri, 15 Oct 1993 10:21:01 +0100 lcp ZF/ind-syntax/refl_thin: new
Thu, 16 Sep 1993 12:20:38 +0200 clasohm Initial revision
less more (0) tip