src/HOL/Product_Type.thy
2015-04-14 Andreas Lochbihler 2015-04-14 add lemmas
2015-03-31 wenzelm 2015-03-31 clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-13 hoelzl 2014-11-13 import general theorems from AFP/Markov_Models
2014-11-07 traytel 2014-11-07 more complete fp_sugars for sum and prod; tuned; removed theorem duplicates; removed obsolete Lifting_{Option,Product,Sum} theories
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-09-29 haftmann 2014-09-29 corrected white-space accident
2014-09-28 haftmann 2014-09-28 tuned
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