src/ZF/add_ind_def.ML
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