src/HOL/Product_Type.thy
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
2011-07-02 haftmann 2011-07-02 install case certificate for If after code_datatype declaration for bool
2011-06-29 wenzelm 2011-06-29 modernized some simproc setup;
2011-06-29 wenzelm 2011-06-29 modernized some simproc setup;
2011-04-19 wenzelm 2011-04-19 eliminated Codegen.mode in favour of explicit argument;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-04-06 wenzelm 2011-04-06 typed_print_translation: discontinued show_sorts argument;
2011-03-24 wenzelm 2011-03-24 added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
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