src/HOL/Tools/datatype_aux.ML
Sun, 01 Mar 2009 23:36:12 +0100 wenzelm use long names for old-style fold combinators;
Wed, 21 Jan 2009 16:47:04 +0100 haftmann binding replaces bstring
Wed, 31 Dec 2008 00:08:13 +0100 wenzelm moved old add_term_vars, add_term_frees etc. to structure OldTerm;
Thu, 25 Sep 2008 20:34:15 +0200 wenzelm explicit checkpoint for low-level (global) theory operations, admits concurrent proofs;
Sun, 18 May 2008 15:04:09 +0200 wenzelm moved global pretty/string_of functions from Sign to Syntax;
Wed, 07 May 2008 10:59:38 +0200 berghofe Functions get_branching_types and get_arities now use fold instead of foldl/r.
Thu, 03 Apr 2008 17:50:50 +0200 berghofe Removed QuickAndDirty constructor from simproc_dist datatype.
Thu, 10 Jan 2008 19:18:14 +0100 berghofe Eliminated DatatypeAux.dest_TFree to avoid clashes
Mon, 17 Dec 2007 18:30:44 +0100 berghofe - Removed redundant head_len field in datatype_info
Tue, 25 Sep 2007 17:06:14 +0200 wenzelm proper Sign operations instead of Theory aliases;
Tue, 25 Sep 2007 12:16:08 +0200 haftmann datatype interpretators for size and datatype_realizer
Wed, 04 Apr 2007 23:29:33 +0200 wenzelm rep_thm/cterm/ctyp: removed obsolete sign field;
Wed, 04 Apr 2007 00:11:03 +0200 wenzelm removed obsolete sign_of/sign_of_thm;
Sat, 18 Nov 2006 00:20:29 +0100 haftmann cleanup
Fri, 13 Oct 2006 18:18:58 +0200 berghofe Adapted to new inductive definition package.
Sun, 11 Jun 2006 21:59:17 +0200 wenzelm avoid unqualified exception;
Sat, 11 Mar 2006 21:23:10 +0100 wenzelm got rid of type Sign.sg;
Sat, 21 Jan 2006 23:02:14 +0100 wenzelm simplified type attribute;
Fri, 09 Dec 2005 09:06:45 +0100 haftmann oriented result pairs in PureThy
Mon, 05 Dec 2005 00:38:07 +0100 berghofe Added store_thmss_atts to signature again.
Thu, 01 Dec 2005 18:39:08 +0100 berghofe Added new component "sorts" to record datatype_info.
Thu, 01 Dec 2005 08:28:02 +0100 haftmann oriented pairs theory * 'a to 'a * theory
Thu, 10 Nov 2005 20:57:11 +0100 wenzelm renamed Thm.cgoal_of to Thm.cprem_of;
Mon, 07 Nov 2005 11:28:34 +0100 berghofe New function store_thmss_atts.
Wed, 02 Nov 2005 23:59:49 +0100 huffman fix spelling
Fri, 28 Oct 2005 22:27:46 +0200 wenzelm Logic.unprotect;
Mon, 19 Sep 2005 16:38:35 +0200 haftmann introduced AList module
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;
Fri, 22 Jul 2005 11:55:11 +0200 berghofe Tuned comment.
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.
Tue, 07 Dec 2004 14:42:08 +0100 webertj comment added
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Tue, 08 Jun 2004 19:23:53 +0200 berghofe Added exception Datatype_Empty.
Mon, 26 Apr 2004 14:54:45 +0200 wenzelm use Syntax.is_identifier;
Wed, 13 Nov 2002 15:27:27 +0100 berghofe name_of_type now replaces non-identifiers by dummy names.
Thu, 10 Oct 2002 14:26:50 +0200 berghofe Reimplemented parts of datatype package dealing with datatypes involving
Fri, 31 Aug 2001 18:46:48 +0200 wenzelm tuned headers;
Mon, 02 Oct 2000 14:21:12 +0200 wenzelm info: weak_case_cong;
Wed, 30 Aug 2000 13:55:26 +0200 berghofe New function name_of_typ.
Mon, 13 Mar 2000 13:22:31 +0100 wenzelm adapted to new PureThy.add_thms etc.;
Fri, 10 Mar 2000 01:13:37 +0100 wenzelm type descr;
Wed, 01 Mar 2000 20:48:57 +0100 wenzelm tuned;
Sun, 27 Feb 2000 15:26:47 +0100 wenzelm HOLogic.dest_conj;
Fri, 16 Jul 1999 12:14:04 +0200 berghofe - Datatype package now also supports arbitrarily branching datatypes
Wed, 17 Mar 1999 16:53:46 +0100 wenzelm Theory.sign_of;
Tue, 12 Jan 1999 13:54:51 +0100 wenzelm eliminated tthm type and Attribute structure;
Mon, 16 Nov 1998 11:14:02 +0100 wenzelm Attribute.tthms_of;
Fri, 16 Oct 1998 18:54:55 +0200 berghofe - Changed structure of name spaces
Fri, 24 Jul 1998 12:50:06 +0200 berghofe New datatype definition package
less more (0) tip