src/HOL/Product_Type.thy
2014-09-19 blanchet 2014-09-19 made new 'primrec' bootstrapping-capable
2014-09-11 blanchet 2014-09-11 renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
2014-09-10 haftmann 2014-09-10 dropped ineffective print_translation which has never been adjusted to check/uncheck-style case patterns
2014-09-06 haftmann 2014-09-06 added various facts
2014-09-05 blanchet 2014-09-05 added 'plugins' option to control which hooks are enabled
2014-08-18 blanchet 2014-08-18 reordered some (co)datatype property names for more consistency
2014-06-12 haftmann 2014-06-12 uniform treatment of trivial unit instances: simplify by default, unfold in code preprocessor
2014-06-10 Andreas Lochbihler 2014-06-10 add type class instances for unit
2014-05-26 blanchet 2014-05-26 got rid of '=:' squiggly
2014-05-20 nipkow 2014-05-20 added unit :: linorder
2014-04-21 haftmann 2014-04-21 swap with qualifier; tuned
2014-04-12 haftmann 2014-04-12 more operations and lemmas
2014-04-10 wenzelm 2014-04-10 modernized simproc_setup; modernized theory setup;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-19 haftmann 2014-03-19 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
2014-03-13 haftmann 2014-03-13 tuned proofs
2014-03-06 blanchet 2014-03-06 renamed 'map_pair' to 'map_prod'
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2014-02-14 blanchet 2014-02-14 aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
2014-02-14 blanchet 2014-02-14 renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
2014-02-14 blanchet 2014-02-14 renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
2014-02-12 blanchet 2014-02-12 tuning
2014-02-12 blanchet 2014-02-12 adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-02-12 blanchet 2014-02-12 avoid duplicate 'case' definitions by first looking up 'Ctr_Sugar'
2014-02-12 blanchet 2014-02-12 se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors * * * cleaner simp/iff sets
2013-12-05 Andreas Lochbihler 2013-12-05 restrict admissibility to non-empty chains to allow more syntax-directed proof rules
2013-10-18 blanchet 2013-10-18 killed most "no_atp", to make Sledgehammer more complete
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-12 wenzelm 2013-04-12 modifiers for classical wrappers operate on Proof.context instead of claset;
2013-03-12 nipkow 2013-03-12 extended set comprehension notation with {pttrn : A . P}
2013-02-17 haftmann 2013-02-17 Sieve of Eratosthenes
2012-11-17 wenzelm 2012-11-17 tuned signature;
2012-11-16 hoelzl 2012-11-16 move theorems to be more generally useable
2012-10-17 bulwahn 2012-10-17 moving Pair_inject from legacy and duplicate section to general section, as Pair_inject was considered a duplicate in e8400e31528a by mistake (cf. communication on dev mailing list)
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-10-10 bulwahn 2012-10-10 moving simproc from Finite_Set to more appropriate Product_Type theory
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-05-24 wenzelm 2012-05-24 tuned proofs;
2012-04-25 blanchet 2012-04-25 added "no_atp"s for extremely prolific, useless facts for ATPs
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2012-02-23 haftmann 2012-02-23 tuned whitespace
2012-02-21 haftmann 2012-02-21 reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
2012-02-20 haftmann 2012-02-20 tuned whitespace
2012-01-01 haftmann 2012-01-01 interaction of set operations for execution and membership predicate
2011-12-29 haftmann 2011-12-29 attribute code_abbrev superseedes code_unfold_post
2011-12-26 haftmann 2011-12-26 moved various set operations to theory Set (resp. Product_Type)
2011-11-30 wenzelm 2011-11-30 prefer typedef without alternative name;
2011-11-30 wenzelm 2011-11-30 prefer typedef without extra definition and alternative name; tuned proofs;
2011-11-28 nipkow 2011-11-28 Hide Product_Type.Times - too precious an identifier
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-10-19 huffman 2011-10-19 merged
2011-10-18 huffman 2011-10-18 hide typedef-generated constants Product_Type.prod and Sum_Type.sum
2011-10-19 bulwahn 2011-10-19 removing old code generator setup of inductive predicates
2011-10-19 bulwahn 2011-10-19 removing old code generator setup for product types
2011-09-13 huffman 2011-09-13 tuned proofs
2011-08-08 huffman 2011-08-08 rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
2011-07-17 haftmann 2011-07-17 moving UNIV = ... equations to their proper theories