src/HOL/Product_Type.thy
Wed, 17 Oct 2012 14:13:57 +0200 bulwahn 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)
Fri, 12 Oct 2012 18:58:20 +0200 wenzelm discontinued obsolete typedef (open) syntax;
Wed, 10 Oct 2012 10:47:43 +0200 bulwahn moving simproc from Finite_Set to more appropriate Product_Type theory
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Thu, 24 May 2012 17:25:53 +0200 wenzelm tuned proofs;
Wed, 25 Apr 2012 00:57:41 +0200 blanchet added "no_atp"s for extremely prolific, useless facts for ATPs
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure;
Thu, 23 Feb 2012 20:15:59 +0100 haftmann tuned whitespace
Tue, 21 Feb 2012 08:15:42 +0100 haftmann reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
Mon, 20 Feb 2012 21:04:00 +0100 haftmann tuned whitespace
Sun, 01 Jan 2012 15:44:15 +0100 haftmann interaction of set operations for execution and membership predicate
Thu, 29 Dec 2011 10:47:55 +0100 haftmann attribute code_abbrev superseedes code_unfold_post
Mon, 26 Dec 2011 18:32:43 +0100 haftmann moved various set operations to theory Set (resp. Product_Type)
Wed, 30 Nov 2011 18:07:14 +0100 wenzelm prefer typedef without alternative name;
Wed, 30 Nov 2011 16:27:10 +0100 wenzelm prefer typedef without extra definition and alternative name;
Mon, 28 Nov 2011 11:22:36 +0100 nipkow Hide Product_Type.Times - too precious an identifier
Sun, 20 Nov 2011 21:07:10 +0100 wenzelm eliminated obsolete "standard";
Wed, 19 Oct 2011 17:45:25 +0200 huffman merged
Tue, 18 Oct 2011 15:19:06 +0200 huffman hide typedef-generated constants Product_Type.prod and Sum_Type.sum
Wed, 19 Oct 2011 08:37:22 +0200 bulwahn removing old code generator setup of inductive predicates
Wed, 19 Oct 2011 08:37:21 +0200 bulwahn removing old code generator setup for product types
Tue, 13 Sep 2011 17:07:33 -0700 huffman tuned proofs
Mon, 08 Aug 2011 10:32:55 -0700 huffman rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
Sun, 17 Jul 2011 19:48:02 +0200 haftmann moving UNIV = ... equations to their proper theories
Sat, 02 Jul 2011 22:55:58 +0200 haftmann install case certificate for If after code_datatype declaration for bool
Wed, 29 Jun 2011 18:12:34 +0200 wenzelm modernized some simproc setup;
Wed, 29 Jun 2011 17:35:46 +0200 wenzelm modernized some simproc setup;
Tue, 19 Apr 2011 23:57:28 +0200 wenzelm eliminated Codegen.mode in favour of explicit argument;
Fri, 08 Apr 2011 13:31:16 +0200 wenzelm explicit structure Syntax_Trans;
Wed, 06 Apr 2011 13:33:46 +0200 wenzelm typed_print_translation: discontinued show_sorts argument;
Thu, 24 Mar 2011 16:56:19 +0100 wenzelm added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
Tue, 22 Mar 2011 12:49:07 +0100 nipkow fixed a printing problem for bounded quantifiers and bounded set operators in the case of tuples
Mon, 21 Feb 2011 10:44:19 +0100 blanchet renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
Tue, 11 Jan 2011 14:12:37 +0100 haftmann "enriched_type" replaces less specific "type_lifting"
Tue, 21 Dec 2010 17:52:23 +0100 haftmann tuned type_lifting declarations
Fri, 17 Dec 2010 17:43:54 +0100 wenzelm replaced command 'nonterminals' by slightly modernized version 'nonterminal';
Mon, 06 Dec 2010 09:19:10 +0100 haftmann replace `type_mapper` by the more adequate `type_lifting`
Fri, 03 Dec 2010 10:03:13 +0100 huffman theorem names generated by the (rep_)datatype command now have mandatory qualifiers
Mon, 22 Nov 2010 10:34:33 +0100 hoelzl Replace surj by abbreviation; remove surj_on.
Thu, 18 Nov 2010 17:01:16 +0100 haftmann map_pair replaces prod_fun
Tue, 16 Nov 2010 16:36:57 -0800 huffman typedef (open) unit
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Fri, 10 Sep 2010 10:21:25 +0200 haftmann Haskell == is infix, not infixl
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Fri, 27 Aug 2010 19:34:23 +0200 haftmann renamed class/constant eq to equal; tuned some instantiations
Wed, 25 Aug 2010 18:36:22 +0200 wenzelm renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
Tue, 13 Jul 2010 18:01:42 +0200 bulwahn correcting function name of generator for products of traditional code generator (introduced in 0040bafffdef)
Mon, 12 Jul 2010 08:58:13 +0200 haftmann dropped superfluous [code del]s
Fri, 09 Jul 2010 08:11:10 +0200 haftmann nicer xsymbol syntax for fcomp and scomp
Sat, 03 Jul 2010 00:50:35 +0200 blanchet adapt Nitpick to "prod_case" and "*" -> "sum" renaming;
Thu, 01 Jul 2010 16:54:44 +0200 haftmann "prod" and "sum" replace "*" and "+" respectively
Mon, 28 Jun 2010 15:03:07 +0200 haftmann merged constants "split" and "prod_case"
Mon, 14 Jun 2010 15:10:36 +0200 haftmann removed simplifier congruence rule of "prod_case"
Thu, 10 Jun 2010 12:24:01 +0200 haftmann qualified type "*"; qualified constants Pair, fst, snd, split
Tue, 08 Jun 2010 16:37:19 +0200 haftmann qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
Wed, 02 Jun 2010 12:40:12 +0200 nipkow added lemmas
Fri, 28 May 2010 13:37:28 +0200 haftmann more coherent theory structure; tuned headings
Wed, 26 May 2010 16:05:25 +0200 haftmann dropped legacy theorem bindings
Wed, 05 May 2010 00:59:59 +0200 krauss repaired comments where SOMEthing went utterly wrong (cf. 2b04504fcb69)
Tue, 20 Apr 2010 17:58:34 +0200 hoelzl Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
less more (0) -100 -60 tip