src/ZF/add_ind_def.ML
Tue, 30 Jan 1996 13:42:57 +0100 clasohm expanded tabs
Fri, 22 Dec 1995 11:09:28 +0100 paulson Improving space efficiency of inductive/datatype definitions.
Thu, 04 May 1995 02:02:18 +0200 lcp Changed to use split instead of fsplit. The weakening of fsplitE appears not
Fri, 25 Nov 1994 11:08:12 +0100 lcp checks that the recursive sets are Consts before taking
Mon, 21 Nov 1994 18:48:03 +0100 lcp ZF INDUCTIVE DEFINITIONS: Simplifying the type checking for mutually
Wed, 14 Sep 1994 16:05:39 +0200 wenzelm replaced lookup_const by Sign.const_type;
Thu, 08 Sep 1994 12:55:50 +0200 lcp ZF/add_ind_def/add_fp_def_i: now prints the fixedpoint defs at the terminal
Fri, 19 Aug 1994 16:12:23 +0200 wenzelm replaced add_defns_i by add_defs_i;
Fri, 12 Aug 1994 12:51:34 +0200 lcp installation of new inductive/datatype sections
less more (0) tip