src/HOL/Product_Type.thy
2016-04-08 wenzelm 2016-04-08 eliminated unused simproc identifier;
2016-03-11 blanchet 2016-03-11 generate theorems like 'bool.split_sel'
2016-02-22 paulson 2016-02-22 An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
2016-01-12 Andreas Lochbihler 2016-01-12 add BNF instance for Dlist
2016-01-08 hoelzl 2016-01-08 add uniform spaces
2015-12-28 wenzelm 2015-12-28 former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
2015-12-27 wenzelm 2015-12-27 discontinued ASCII replacement syntax <*>;
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-11 Andreas Lochbihler 2015-11-11 add various lemmas
2015-10-13 haftmann 2015-10-13 restored print translation from a1141fb798ff, to prevent a printing misfit observable using "thm divmod_nat_if" in theory "Divides", with a meagure indication in the comment
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-10-13 haftmann 2015-10-13 moved lemmas
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2015-09-22 haftmann 2015-09-22 effective revert of e6b1236f9b3d: spontaneous eta-contraction happens on the print translation level and can only be suppressed on the print translation level
2015-09-09 wenzelm 2015-09-09 simplified simproc programming interfaces;
2015-09-06 haftmann 2015-09-06 tuned notation, proofs, namespace
2015-09-06 haftmann 2015-09-06 obsolete: if case_prod is fully applied, it is printed as proper case expression; eta-contracted variants are read best as "uncurry" combinator
2015-09-06 haftmann 2015-09-06 prefer "uncurry" as canonical name for case distinction on products in combinatorial view
2015-09-06 haftmann 2015-09-06 tuned
2015-09-06 haftmann 2015-09-06 obsolete: all (formally unchecked) examples given in the comments work out of the box as advertised
2015-09-06 haftmann 2015-09-06 dropped whitespace leftover from b57df8eecad6
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-08-27 haftmann 2015-08-27 standardized some occurences of ancient "split" alias
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
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_...'