src/ZF/Tools/datatype_package.ML
Tue, 18 Nov 2008 18:25:42 +0100 wenzelm eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion;
Thu, 23 Oct 2008 16:07:03 +0200 wenzelm Thm.get_def;
Tue, 02 Sep 2008 14:10:45 +0200 wenzelm explicit type Name.binding for higher-specification elements;
Tue, 29 Jul 2008 08:15:40 +0200 haftmann PureThy: dropped note_thmss_qualified, dropped _i suffix
Wed, 18 Jun 2008 18:55:10 +0200 wenzelm eliminated old Sign.read_term/Thm.read_cterm etc.;
Sun, 18 May 2008 15:04:09 +0200 wenzelm moved global pretty/string_of functions from Sign to Syntax;
Wed, 19 Mar 2008 22:27:57 +0100 wenzelm renamed datatype thmref to Facts.ref, tuned interfaces;
Sat, 01 Mar 2008 15:01:03 +0100 wenzelm tuned ML code, more antiquotations;
Sat, 01 Mar 2008 14:10:15 +0100 wenzelm misc cleanup of embedded ML code;
Mon, 11 Feb 2008 15:40:21 +0100 krauss Made theory names in ZF disjoint from HOL theory names to allow loading both developments
Sat, 26 Jan 2008 20:01:37 +0100 wenzelm avoid redundant escaping of Isabelle symbols;
Sun, 07 Oct 2007 21:19:31 +0200 wenzelm modernized specifications;
Sat, 06 Oct 2007 16:50:04 +0200 wenzelm simplified interfaces for outer syntax;
Wed, 03 Oct 2007 22:33:17 +0200 wenzelm avoid unnamed infixes;
Wed, 26 Sep 2007 19:18:00 +0200 wenzelm Attrib.eval_thms;
Tue, 25 Sep 2007 17:06:14 +0200 wenzelm proper Sign operations instead of Theory aliases;
Tue, 25 Sep 2007 13:28:37 +0200 wenzelm Syntax.parse/check/read;
Tue, 14 Aug 2007 13:20:12 +0200 wenzelm PrimitiveDefs.mk_defpair;
Tue, 19 Jun 2007 23:15:38 +0200 wenzelm BalancedTree;
Wed, 04 Apr 2007 00:11:03 +0200 wenzelm removed obsolete sign_of/sign_of_thm;
Fri, 19 Jan 2007 22:08:08 +0100 wenzelm moved parts of OuterParse to SpecParse;
Tue, 14 Nov 2006 00:15:38 +0100 wenzelm incorporated IsarThy into IsarCmd;
Sat, 08 Jul 2006 12:54:33 +0200 wenzelm Goal.prove_global;
Sat, 21 Jan 2006 23:02:14 +0100 wenzelm simplified type attribute;
Sun, 15 Jan 2006 19:58:53 +0100 wenzelm classical attributes: optional weight;
Sat, 14 Jan 2006 22:25:34 +0100 wenzelm generic attributes;
Fri, 16 Dec 2005 09:00:11 +0100 haftmann re-arranged tuples (theory * 'a) to ('a * theory) in Pure
Fri, 09 Dec 2005 09:06:45 +0100 haftmann oriented result pairs in PureThy
Tue, 06 Dec 2005 09:04:09 +0100 haftmann re-oriented some result tuples in PureThy
Wed, 16 Nov 2005 17:45:31 +0100 wenzelm Term.betapplys;
Tue, 25 Oct 2005 18:18:49 +0200 wenzelm avoid legacy goals;
Fri, 21 Oct 2005 18:14:38 +0200 wenzelm OldGoals;
Wed, 19 Oct 2005 21:52:49 +0200 wenzelm removed obsolete add_datatype_x;
Thu, 15 Sep 2005 17:16:56 +0200 wenzelm TableFun/Symtab: curried lookup and update;
Mon, 05 Sep 2005 17:38:18 +0200 wenzelm curried_lookup/update;
Tue, 16 Aug 2005 13:42:26 +0200 wenzelm OuterKeyword;
Wed, 13 Apr 2005 18:45:25 +0200 wenzelm *** MESSAGE REFERS TO PREVIOUS VERSION ***
Wed, 13 Apr 2005 18:34:22 +0200 wenzelm *** empty log message ***
Fri, 04 Mar 2005 15:07:34 +0100 skalberg Removed practically all references to Library.foldr.
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Mon, 24 Jan 2005 18:12:22 +0100 berghofe Replaced xstring by thmref.
Wed, 15 May 2002 10:44:58 +0200 paulson better error messages for datatypes not declared Const
Tue, 12 Feb 2002 20:28:27 +0100 wenzelm got rid of explicit marginal comments (now stripped earlier from input);
Mon, 19 Nov 2001 20:47:57 +0100 wenzelm tuned;
Fri, 16 Nov 2001 22:08:55 +0100 wenzelm additional P.marg_comment;
Wed, 14 Nov 2001 23:18:13 +0100 wenzelm use proper intr_names (for required case_names);
Wed, 14 Nov 2001 18:46:30 +0100 wenzelm adapted primrec/datatype to Isar;
Fri, 09 Nov 2001 22:53:10 +0100 wenzelm adapted to add_inductive_x;
Thu, 13 Jul 2000 23:20:57 +0200 wenzelm adapted PureThy.add_defs_i;
Fri, 05 May 2000 22:37:04 +0200 wenzelm use Sign.simple_read_term;
Mon, 13 Mar 2000 13:28:31 +0100 wenzelm adapted to new PureThy.add_thms etc.;
Thu, 13 Jan 2000 17:34:39 +0100 paulson change in add_thmss to suppress warning
Mon, 04 Oct 1999 21:39:36 +0200 wenzelm tuned;
Wed, 27 Jan 1999 15:58:22 +0100 paulson automatic insertion of datatype intr rules into claset
Tue, 19 Jan 1999 11:18:11 +0100 paulson removal of the (thm list) argument of mk_cases
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;
Tue, 12 Jan 1999 13:54:51 +0100 wenzelm eliminated tthm type and Attribute structure;
Thu, 07 Jan 1999 18:30:55 +0100 paulson ZF: the natural numbers as a datatype
less more (0) -60 tip