src/HOL/Tools/Datatype/datatype_data.ML
2014-05-05 blanchet 2014-05-05 simplify selectors in code views
2014-04-03 blanchet 2014-04-03 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
2014-03-06 wenzelm 2014-03-06 more rigid type_name demands, based on educated guesses about the tools involved here;
2014-03-06 wenzelm 2014-03-06 tuned signature -- more uniform check_type_name/read_type_name; proper reports for read_type_name (lost in 710bc66f432c);
2014-02-26 wenzelm 2014-02-26 tuned signature;
2014-02-12 blanchet 2014-02-12 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')
2014-01-02 blanchet 2014-01-02 generate 'disc_iff' property in 'primcorec'
2013-11-19 blanchet 2013-11-19 case_if -> case_eq_if + docs
2013-11-13 blanchet 2013-11-13 shortened generated property name
2013-11-12 blanchet 2013-11-12 register old-style datatypes as 'Ctr_Sugar'
2011-12-15 wenzelm 2011-12-15 clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
2011-12-15 wenzelm 2011-12-15 separate rep_datatype.ML; tuned signature;
2011-12-15 wenzelm 2011-12-15 misc tuning and simplification;
2011-12-14 wenzelm 2011-12-14 tuned signature;
2011-12-14 wenzelm 2011-12-14 avoid fragile Sign.intern_const -- pass internal names directly; tuned;
2011-12-13 wenzelm 2011-12-13 'datatype' specifications allow explicit sort constraints; tuned signatures;
2011-12-12 wenzelm 2011-12-12 datatype dtyp with explicit sort information; tuned messages;
2011-12-12 wenzelm 2011-12-12 tuned;
2011-12-02 wenzelm 2011-12-02 eliminated some legacy operations;
2011-11-30 wenzelm 2011-11-30 discontinued obsolete datatype "alt_names";
2011-11-30 wenzelm 2011-11-30 misc tuning;
2011-11-23 wenzelm 2011-11-23 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-11-09 wenzelm 2011-11-09 misc tuning;
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-06-27 wenzelm 2011-06-27 merged
2011-06-27 krauss 2011-06-27 new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor; renamed old version to info_of_constr_permissive, reflecting its semantics
2011-06-27 wenzelm 2011-06-27 document antiquotations are managed as theory data, with proper name space and entity markup;
2011-06-09 wenzelm 2011-06-09 tuned signature: Name.invent and Name.invent_names;
2011-06-09 wenzelm 2011-06-09 simplified Name.variant -- discontinued builtin fold_map;
2011-06-08 krauss 2011-06-08 removed generation of instantiated pattern set, which is never actually used
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-16 wenzelm 2011-04-16 prefer local name spaces; tuned signatures; tuned;
2011-04-08 wenzelm 2011-04-08 discontinued Syntax.max_pri, which is not really a symbolic parameter;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
2011-04-08 wenzelm 2011-04-08 discontinued special status of structure Printer;
2011-01-10 wenzelm 2011-01-10 standardized split_last/last_elem towards List.last; eliminated obsolete Library.last_elem;
2010-12-30 wenzelm 2010-12-30 do not open auxiliary ML structures;
2010-12-04 wenzelm 2010-12-04 tuned @{datatype} using Syntax.pretty_priority (NB: postfix type application yields Syntax.max_pri, so arguments in prefix application require higher priority);
2010-12-03 huffman 2010-12-03 theorem names generated by the (rep_)datatype command now have mandatory qualifiers
2010-12-01 wenzelm 2010-12-01 more direct use of binder_types/body_type;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-08-27 wenzelm 2010-08-27 proper context for various Thy_Output options, via official configuration options in ML and Isar;
2010-08-26 wenzelm 2010-08-26 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;
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-30 wenzelm 2010-04-30 slightly more standard induct_simp_add/del attributes; provide explicit context for internal addsimps;
2010-04-25 wenzelm 2010-04-25 modernized naming conventions of main Isar proof elements;
2010-02-25 wenzelm 2010-02-25 clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
2010-02-21 wenzelm 2010-02-21 slightly more abstract syntax mark/unmark operations;
2010-02-21 wenzelm 2010-02-21 adapted to authentic syntax;
2010-02-14 wenzelm 2010-02-14 formal markup of constants;
2010-01-10 berghofe 2010-01-10 Injectivity / distinctness theorems are now used to simplify induction rules.
2009-12-02 haftmann 2009-12-02 tuned
2009-11-30 haftmann 2009-11-30 dropped some unused bindings
2009-11-30 haftmann 2009-11-30 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
2009-11-27 haftmann 2009-11-27 renamed former datatype.ML to datatype_data.ML
2009-11-27 haftmann 2009-11-27 renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML