src/ZF/ind_syntax.ML
Wed, 17 Aug 2011 18:05:31 +0200 wenzelm modernized signature of Term.absfree/absdummy;
Mon, 20 Dec 2010 16:44:33 +0100 wenzelm proper identifiers for consts and types;
Sun, 12 Sep 2010 19:04:02 +0200 wenzelm eliminated aliases of Type.constraint;
Wed, 18 Aug 2010 12:19:27 +0200 haftmann deglobalization
Thu, 27 May 2010 17:41:27 +0200 wenzelm renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
Mon, 15 Feb 2010 17:17:51 +0100 wenzelm discontinued unnamed infix syntax;
Sun, 07 Feb 2010 19:33:34 +0100 wenzelm renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
Thu, 29 Oct 2009 17:58:26 +0100 wenzelm standardized filter/filter_out;
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Sat, 17 Oct 2009 00:52:37 +0200 wenzelm explicitly qualify Drule.standard;
Thu, 15 Oct 2009 23:28:10 +0200 wenzelm replaced String.concat by implode;
Tue, 29 Sep 2009 22:48:24 +0200 wenzelm modernized Balanced_Tree;
Tue, 29 Sep 2009 16:24:36 +0200 wenzelm explicit indication of Unsynchronized.ref;
Sat, 07 Mar 2009 22:17:25 +0100 wenzelm more uniform handling of binding in packages;
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Wed, 18 Jun 2008 18:55:10 +0200 wenzelm eliminated old Sign.read_term/Thm.read_cterm etc.;
Mon, 16 Jun 2008 22:13:39 +0200 wenzelm pervasive RuleInsts;
Mon, 16 Jun 2008 17:54:43 +0200 wenzelm RuleInsts.read_instantiate;
Wed, 11 Jun 2008 18:02:00 +0200 wenzelm Drule.read_instantiate;
Sun, 18 May 2008 15:04:09 +0200 wenzelm moved global pretty/string_of functions from Sign to Syntax;
Sat, 01 Mar 2008 14:10:15 +0100 wenzelm misc cleanup of embedded ML code;
Mon, 11 Feb 2008 21:32:12 +0100 wenzelm removed unnecessary theory qualifiers;
Mon, 11 Feb 2008 15:40:21 +0100 krauss Made theory names in ZF disjoint from HOL theory names to allow loading both developments
Sun, 07 Oct 2007 21:19:31 +0200 wenzelm modernized specifications;
Wed, 03 Oct 2007 22:33:17 +0200 wenzelm avoid unnamed infixes;
Tue, 19 Jun 2007 23:15:38 +0200 wenzelm BalancedTree;
Thu, 31 May 2007 14:34:07 +0200 wenzelm removed obsolete IFOL.thy/FOL.thy values;
Tue, 03 Apr 2007 19:24:11 +0200 wenzelm removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
Sun, 26 Nov 2006 23:43:53 +0100 wenzelm converted legacy ML scripts;
Wed, 16 Nov 2005 17:45:22 +0100 wenzelm Term.betapply;
Tue, 25 Oct 2005 18:18:59 +0200 wenzelm traceIt: plain term;
Fri, 15 Jul 2005 15:44:22 +0200 wenzelm tuned fold on terms and lists;
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Wed, 15 May 2002 10:44:58 +0200 paulson better error messages for datatypes not declared Const
Mon, 19 Nov 2001 20:47:57 +0100 wenzelm tuned;
Fri, 05 May 2000 22:37:04 +0200 wenzelm use Sign.simple_read_term;
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.
less more (0) -60 tip