src/ZF/ind_syntax.ML
Mon, 04 Oct 1999 21:37:35 +0200 wenzelm tryres, gen_make_elim moved here;
Wed, 13 Jan 1999 11:57:09 +0100 paulson datatype package improvements
Tue, 12 Jan 1999 15:17:37 +0100 wenzelm eliminated global/local names;
Mon, 28 Dec 1998 16:59:28 +0100 paulson new inductive, datatype and primrec packages, etc.
Wed, 27 May 1998 12:23:45 +0200 paulson mk_all_imp: no longer creates goals that have beta-redexes
Fri, 10 Apr 1998 13:15:28 +0200 paulson Fixed bug in inductive sections to allow disjunctive premises;
Wed, 03 Dec 1997 10:52:17 +0100 paulson Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
Fri, 17 Oct 1997 17:42:39 +0200 wenzelm (co) inductive / datatype package adapted to qualified names;
Thu, 28 Nov 1996 10:44:24 +0100 paulson Replaced map...~~ by ListPair.map
Tue, 26 Nov 1996 16:11:18 +0100 paulson Eta-expansion of a function definition, for value polymorphism
Wed, 08 May 1996 18:01:54 +0200 paulson moved ap_split to cartprod.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, 24 Nov 1994 10:57:24 +0100 lcp data_domain,Codata_domain: removed replicate; now return one
Thu, 25 Aug 1994 12:09:21 +0200 lcp ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
Fri, 19 Aug 1994 16:13:53 +0200 wenzelm replaced Lexicon.scan_id by Scanner.scan_id;
Thu, 18 Aug 1994 17:41:40 +0200 lcp ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
Fri, 12 Aug 1994 12:51:34 +0200 lcp installation of new inductive/datatype sections
Tue, 12 Jul 1994 14:26:04 +0200 clasohm removed flatten_typ and replaced add_consts by add_consts_i
Mon, 11 Jul 1994 13:15:05 +0200 clasohm removed flatten_term and replaced add_axioms by add_axioms_i
Fri, 01 Jul 1994 11:03:42 +0200 clasohm replaced extend_theory by new add_* functions;
Tue, 21 Jun 1994 17:20:34 +0200 lcp Addition of cardinals and order types, various tidying
Tue, 18 Jan 1994 16:37:12 +0100 lcp Updated refs to old Sign functions
Tue, 21 Dec 1993 16:38:45 +0100 nipkow added []-field to extend_theory: no type abbreviations.
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, 30 Sep 1993 10:10:21 +0100 lcp ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
Fri, 17 Sep 1993 16:16:38 +0200 lcp Installation of new simplifier for ZF. Deleted all congruence rules not
Thu, 16 Sep 1993 12:20:38 +0200 clasohm Initial revision
less more (0) tip