src/HOL/Datatype.thy
Fri, 21 Feb 2014 00:09:56 +0100 blanchet adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
Wed, 12 Feb 2014 08:37:06 +0100 blanchet adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed 'nat_{case,rec}' to '{case,rec}_nat'
Tue, 12 Nov 2013 13:47:24 +0100 blanchet moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
Fri, 12 Oct 2012 18:58:20 +0200 wenzelm discontinued obsolete typedef (open) syntax;
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Sun, 15 Apr 2012 20:51:07 +0200 haftmann centralized enriched_type declaration, thanks to in-situ available Isar commands
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure;
Wed, 30 Nov 2011 16:27:10 +0100 wenzelm prefer typedef without extra definition and alternative name;
Sun, 20 Nov 2011 21:07:10 +0100 wenzelm eliminated obsolete "standard";
Wed, 30 Mar 2011 11:32:52 +0200 bulwahn renewing specifications in HOL: replacing types by type_synonym
Tue, 11 Jan 2011 14:12:37 +0100 haftmann "enriched_type" replaces less specific "type_lifting"
Tue, 21 Dec 2010 17:52:23 +0100 haftmann tuned type_lifting declarations
Mon, 06 Dec 2010 09:25:05 +0100 haftmann moved bootstrap of type_lifting to Fun
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Fri, 16 Apr 2010 21:28:09 +0200 wenzelm replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
Thu, 18 Feb 2010 14:21:44 -0800 huffman get rid of many duplicate simp rule warnings
Mon, 30 Nov 2009 11:42:49 +0100 haftmann modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
Fri, 27 Nov 2009 08:41:10 +0100 haftmann renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
Wed, 25 Nov 2009 11:16:57 +0100 haftmann bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
Thu, 12 Nov 2009 15:49:01 +0100 haftmann explicit code lemmas produce nices code
Wed, 04 Mar 2009 10:47:20 +0100 nipkow Made Option a separate theory and renamed option_map to Option.map
Wed, 21 Jan 2009 23:40:23 +0100 haftmann changed import hierarchy
Wed, 21 Jan 2009 16:47:31 +0100 haftmann dropped ID
Sat, 27 Dec 2008 17:49:15 +0100 krauss removed duplicate sum_case used only by function package;
Tue, 09 Dec 2008 15:31:38 -0800 huffman move lemmas from Numeral_Type.thy to other theories
Fri, 24 Oct 2008 17:51:35 +0200 haftmann more clever module names for code generation
Fri, 10 Oct 2008 06:45:53 +0200 haftmann `code func` now just `code`
Tue, 07 Oct 2008 16:07:50 +0200 haftmann arbitrary is undefined
Thu, 25 Sep 2008 09:28:03 +0200 haftmann discontinued special treatment of op = vs. eq_class.eq
Sun, 24 Aug 2008 14:42:22 +0200 haftmann tuned import order
Mon, 11 Aug 2008 14:49:53 +0200 haftmann moved class wellorder to theory Orderings
Tue, 10 Jun 2008 15:30:33 +0200 haftmann rep_datatype command now takes list of constructors as input arguments
Fri, 25 Apr 2008 15:30:33 +0200 krauss Merged theories about wellfoundedness into one: Wellfounded.thy
Thu, 20 Mar 2008 12:02:52 +0100 haftmann Product_Type.apfst and Product_Type.apsnd
Wed, 19 Mar 2008 22:47:35 +0100 wenzelm eliminated change_claset/simpset;
Tue, 26 Feb 2008 20:38:10 +0100 haftmann tuned proofs
Fri, 15 Feb 2008 16:09:12 +0100 haftmann <= and < on nat no longer depend on wellfounded relations
Sat, 05 Jan 2008 09:16:27 +0100 haftmann more instantiation
Mon, 17 Dec 2007 18:22:48 +0100 berghofe Removed obsolete lemma size_sum.
Wed, 05 Dec 2007 14:15:45 +0100 haftmann simplified infrastructure for code generator operational equality
Fri, 30 Nov 2007 20:13:05 +0100 haftmann more canonical attribute application
Thu, 04 Oct 2007 19:54:46 +0200 haftmann tuned datatype_codegen setup
Wed, 26 Sep 2007 20:27:55 +0200 haftmann moved Finite_Set before Datatype
Tue, 25 Sep 2007 12:16:08 +0200 haftmann datatype interpretators for size and datatype_realizer
Wed, 15 Aug 2007 12:52:56 +0200 paulson ATP blacklisting is now in theory data, attribute noatp
Thu, 09 Aug 2007 15:52:42 +0200 haftmann re-eliminated Option.thy
Tue, 07 Aug 2007 09:38:44 +0200 haftmann split off theory Option for benefit of code generator
Wed, 09 May 2007 07:53:06 +0200 haftmann moved recfun_codegen.ML to Code_Generator.thy
Tue, 24 Apr 2007 15:18:09 +0200 berghofe Added intro / elim rules for prod_case.
Fri, 20 Apr 2007 11:21:42 +0200 haftmann Isar definitions are now added explicitly to code theorem table
Wed, 11 Apr 2007 08:28:13 +0200 haftmann dropped legacy ML bindings
Fri, 09 Mar 2007 08:45:55 +0100 haftmann *** empty log message ***
Fri, 02 Feb 2007 15:47:58 +0100 nipkow a few additions and deletions
Wed, 27 Dec 2006 19:09:54 +0100 haftmann removed code generation stuff belonging to other theories
Wed, 06 Dec 2006 01:12:36 +0100 wenzelm removed legacy ML bindings;
Wed, 22 Nov 2006 10:20:12 +0100 haftmann dropped eq const
Sat, 18 Nov 2006 00:20:13 +0100 haftmann reduced verbosity
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
less more (0) -100 -60 tip