src/HOL/Tools/Datatype/datatype_data.ML
Mon, 01 Sep 2014 16:17:46 +0200 blanchet tuned structure inclusion
Mon, 18 Aug 2014 17:19:58 +0200 blanchet reordered some (co)datatype property names for more consistency
Mon, 05 May 2014 09:30:20 +0200 blanchet simplify selectors in code views
Thu, 03 Apr 2014 10:51:22 +0200 blanchet use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
Thu, 06 Mar 2014 12:43:29 +0100 wenzelm more rigid type_name demands, based on educated guesses about the tools involved here;
Thu, 06 Mar 2014 12:10:19 +0100 wenzelm tuned signature -- more uniform check_type_name/read_type_name;
Wed, 26 Feb 2014 10:53:19 +0100 wenzelm tuned signature;
Wed, 12 Feb 2014 17:36:00 +0100 blanchet iteration n in the 'default' vs. 'update_new' vs. 'update' saga -- 'update' makes sense now that we honor the canonical order on 'merge' (as opposed to raising 'DUP')
Thu, 02 Jan 2014 09:50:22 +0100 blanchet generate 'disc_iff' property in 'primcorec'
Tue, 19 Nov 2013 14:33:20 +0100 blanchet case_if -> case_eq_if + docs
Wed, 13 Nov 2013 12:32:26 +0100 blanchet shortened generated property name
Tue, 12 Nov 2013 13:47:24 +0100 blanchet register old-style datatypes as 'Ctr_Sugar'
Thu, 15 Dec 2011 18:08:40 +0100 wenzelm clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
Thu, 15 Dec 2011 17:37:14 +0100 wenzelm separate rep_datatype.ML;
Thu, 15 Dec 2011 14:11:57 +0100 wenzelm misc tuning and simplification;
Wed, 14 Dec 2011 22:10:04 +0100 wenzelm tuned signature;
Wed, 14 Dec 2011 21:54:32 +0100 wenzelm avoid fragile Sign.intern_const -- pass internal names directly;
Tue, 13 Dec 2011 23:23:51 +0100 wenzelm 'datatype' specifications allow explicit sort constraints;
Mon, 12 Dec 2011 23:05:21 +0100 wenzelm datatype dtyp with explicit sort information;
Mon, 12 Dec 2011 20:55:57 +0100 wenzelm tuned;
Fri, 02 Dec 2011 14:26:43 +0100 wenzelm eliminated some legacy operations;
Wed, 30 Nov 2011 23:30:08 +0100 wenzelm discontinued obsolete datatype "alt_names";
Wed, 30 Nov 2011 21:14:01 +0100 wenzelm misc tuning;
Wed, 23 Nov 2011 22:59:39 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Wed, 09 Nov 2011 21:36:18 +0100 wenzelm misc tuning;
Wed, 10 Aug 2011 20:53:43 +0200 wenzelm old term operations are legacy;
Mon, 27 Jun 2011 22:44:44 +0200 wenzelm merged
Mon, 27 Jun 2011 17:04:04 +0200 krauss new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
Mon, 27 Jun 2011 22:20:49 +0200 wenzelm document antiquotations are managed as theory data, with proper name space and entity markup;
Thu, 09 Jun 2011 20:22:22 +0200 wenzelm tuned signature: Name.invent and Name.invent_names;
Thu, 09 Jun 2011 17:51:49 +0200 wenzelm simplified Name.variant -- discontinued builtin fold_map;
Wed, 08 Jun 2011 00:01:20 +0200 krauss removed generation of instantiated pattern set, which is never actually used
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Sat, 16 Apr 2011 15:25:25 +0200 wenzelm prefer local name spaces;
Fri, 08 Apr 2011 21:11:29 +0200 wenzelm discontinued Syntax.max_pri, which is not really a symbolic parameter;
Fri, 08 Apr 2011 16:34:14 +0200 wenzelm discontinued special treatment of structure Lexicon;
Fri, 08 Apr 2011 15:48:14 +0200 wenzelm discontinued special status of structure Printer;
Mon, 10 Jan 2011 15:19:48 +0100 wenzelm standardized split_last/last_elem towards List.last;
Thu, 30 Dec 2010 23:42:06 +0100 wenzelm do not open auxiliary ML structures;
Sat, 04 Dec 2010 14:59:25 +0100 wenzelm tuned @{datatype} using Syntax.pretty_priority (NB: postfix type application yields Syntax.max_pri, so arguments in prefix application require higher priority);
Fri, 03 Dec 2010 10:03:13 +0100 huffman theorem names generated by the (rep_)datatype command now have mandatory qualifiers
Wed, 01 Dec 2010 15:03:44 +0100 wenzelm more direct use of binder_types/body_type;
Mon, 20 Sep 2010 16:05:25 +0200 wenzelm renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
Fri, 27 Aug 2010 12:40:20 +0200 wenzelm proper context for various Thy_Output options, via official configuration options in ML and Isar;
Thu, 26 Aug 2010 13:09:12 +0200 wenzelm renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
Mon, 31 May 2010 21:06:57 +0200 wenzelm modernized some structure names, keeping a few legacy aliases;
Mon, 17 May 2010 23:54:15 +0200 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
Mon, 03 May 2010 14:25:56 +0200 wenzelm renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
Fri, 30 Apr 2010 23:43:09 +0200 wenzelm slightly more standard induct_simp_add/del attributes;
Sun, 25 Apr 2010 15:52:03 +0200 wenzelm modernized naming conventions of main Isar proof elements;
Thu, 25 Feb 2010 22:06:43 +0100 wenzelm clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
Sun, 21 Feb 2010 22:35:02 +0100 wenzelm slightly more abstract syntax mark/unmark operations;
Sun, 21 Feb 2010 21:10:01 +0100 wenzelm adapted to authentic syntax;
Sun, 14 Feb 2010 00:26:48 +0100 wenzelm formal markup of constants;
Sun, 10 Jan 2010 18:11:00 +0100 berghofe Injectivity / distinctness theorems are now used to simplify induction rules.
Wed, 02 Dec 2009 11:29:49 +0100 haftmann tuned
Mon, 30 Nov 2009 12:28:12 +0100 haftmann dropped some unused bindings
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:42:34 +0100 haftmann renamed former datatype.ML to datatype_data.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
less more (0) tip