src/HOL/Product_Type.thy
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
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