src/HOL/Product_Type.thy
2011-03-22 nipkow 2011-03-22 fixed a printing problem for bounded quantifiers and bounded set operators in the case of tuples
2011-02-21 blanchet 2011-02-21 renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
2011-01-11 haftmann 2011-01-11 "enriched_type" replaces less specific "type_lifting"
2010-12-21 haftmann 2010-12-21 tuned type_lifting declarations
2010-12-17 wenzelm 2010-12-17 replaced command 'nonterminals' by slightly modernized version 'nonterminal';
2010-12-06 haftmann 2010-12-06 replace `type_mapper` by the more adequate `type_lifting`
2010-12-03 huffman 2010-12-03 theorem names generated by the (rep_)datatype command now have mandatory qualifiers
2010-11-22 hoelzl 2010-11-22 Replace surj by abbreviation; remove surj_on.
2010-11-18 haftmann 2010-11-18 map_pair replaces prod_fun
2010-11-16 huffman 2010-11-16 typedef (open) unit
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-10 haftmann 2010-09-10 Haskell == is infix, not infixl
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-07-13 bulwahn 2010-07-13 correcting function name of generator for products of traditional code generator (introduced in 0040bafffdef)
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-07-09 haftmann 2010-07-09 nicer xsymbol syntax for fcomp and scomp
2010-07-03 blanchet 2010-07-03 adapt Nitpick to "prod_case" and "*" -> "sum" renaming; the code in "Nitpick_Preproc", which sorted the types using "typ_ord", was wrong and evil; it seems to have worked only because "*" was called "*"
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-06-28 haftmann 2010-06-28 merged constants "split" and "prod_case"
2010-06-14 haftmann 2010-06-14 removed simplifier congruence rule of "prod_case"
2010-06-10 haftmann 2010-06-10 qualified type "*"; qualified constants Pair, fst, snd, split
2010-06-08 haftmann 2010-06-08 qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
2010-06-02 nipkow 2010-06-02 added lemmas
2010-05-28 haftmann 2010-05-28 more coherent theory structure; tuned headings
2010-05-26 haftmann 2010-05-26 dropped legacy theorem bindings
2010-05-05 krauss 2010-05-05 repaired comments where SOMEthing went utterly wrong (cf. 2b04504fcb69)
2010-04-20 hoelzl 2010-04-20 Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-03-18 blanchet 2010-03-18 merged
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-03-18 haftmann 2010-03-18 lemma swap_inj_on, swap_product
2010-03-02 wenzelm 2010-03-02 proper (type_)notation;
2010-02-25 wenzelm 2010-02-25 modernized structure Split_Rule; tuned signature; more antiquotations;
2010-02-25 wenzelm 2010-02-25 more antiquotations;
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
2010-01-14 haftmann 2010-01-14 tuned for products vs. tupled functions
2010-01-13 haftmann 2010-01-13 some syntax setup for Scala
2009-11-25 haftmann 2009-11-25 bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
2009-11-12 hoelzl 2009-11-12 Renamed upd_snd_conv to apsnd_conv to be consistent with apfst_conv; Added apsnd_apfst_commute
2009-11-10 haftmann 2009-11-10 lemmas about apfst and apsnd
2009-10-28 haftmann 2009-10-28 load Product_Type before Nat; dropped junk
2009-10-28 paulson 2009-10-28 New theory Probability, which contains a development of measure theory
2009-10-24 wenzelm 2009-10-24 import theory Nat here, which avoids duplicate definition of datatype_realizers (and thus allows to maintain fully authentic fact table);
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-07-15 wenzelm 2009-07-15 more antiquotations;
2009-06-23 haftmann 2009-06-23 uniformly capitialized names for subdirectories
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-06-16 haftmann 2009-06-16 dropped ID
2009-06-10 haftmann 2009-06-10 separate directory for datatype package
2009-05-19 haftmann 2009-05-19 pretty printing of functional combinators for evaluation code
2009-04-15 haftmann 2009-04-15 default instantiation for unit type
2009-03-20 berghofe 2009-03-20 split_codegen now eta-expands terms on-the-fly.
2008-11-06 nipkow 2008-11-06 added lemma
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-10-09 haftmann 2008-10-09 established canonical argument order in SML code generators
2008-09-25 haftmann 2008-09-25 discontinued special treatment of op = vs. eq_class.eq
2008-09-17 wenzelm 2008-09-17 back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
2008-06-10 haftmann 2008-06-10 rep_datatype command now takes list of constructors as input arguments