src/HOL/Product_Type.thy
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.
Fri, 16 Apr 2010 21:28:09 +0200 wenzelm replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
Thu, 18 Mar 2010 13:59:20 +0100 blanchet merged
Thu, 18 Mar 2010 12:58:52 +0100 blanchet now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
Thu, 18 Mar 2010 13:56:34 +0100 haftmann lemma swap_inj_on, swap_product
Tue, 02 Mar 2010 23:59:54 +0100 wenzelm proper (type_)notation;
Thu, 25 Feb 2010 22:46:52 +0100 wenzelm modernized structure Split_Rule;
Thu, 25 Feb 2010 22:32:09 +0100 wenzelm more antiquotations;
Thu, 11 Feb 2010 23:00:22 +0100 wenzelm modernized translations;
Thu, 14 Jan 2010 17:47:39 +0100 haftmann tuned for products vs. tupled functions
Wed, 13 Jan 2010 08:56:15 +0100 haftmann some syntax setup for Scala
Wed, 25 Nov 2009 11:16:57 +0100 haftmann bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
Thu, 12 Nov 2009 17:21:43 +0100 hoelzl Renamed upd_snd_conv to apsnd_conv to be consistent with apfst_conv; Added apsnd_apfst_commute
Tue, 10 Nov 2009 16:11:39 +0100 haftmann lemmas about apfst and apsnd
Wed, 28 Oct 2009 17:44:03 +0100 haftmann load Product_Type before Nat; dropped junk
Wed, 28 Oct 2009 11:42:31 +0000 paulson New theory Probability, which contains a development of measure theory
Sat, 24 Oct 2009 18:55:27 +0200 wenzelm import theory Nat here, which avoids duplicate definition of datatype_realizers (and thus allows to maintain fully authentic fact table);
Thu, 15 Oct 2009 23:28:10 +0200 wenzelm replaced String.concat by implode;
Wed, 15 Jul 2009 23:48:21 +0200 wenzelm more antiquotations;
Tue, 23 Jun 2009 12:09:30 +0200 haftmann uniformly capitialized names for subdirectories
Fri, 19 Jun 2009 17:23:21 +0200 haftmann discontinued ancient tradition to suffix certain ML module names with "_package"
Tue, 16 Jun 2009 16:36:56 +0200 haftmann dropped ID
Wed, 10 Jun 2009 15:04:33 +0200 haftmann separate directory for datatype package
Tue, 19 May 2009 13:57:31 +0200 haftmann pretty printing of functional combinators for evaluation code
Wed, 15 Apr 2009 15:30:38 +0200 haftmann default instantiation for unit type
Fri, 20 Mar 2009 10:43:53 +0100 berghofe split_codegen now eta-expands terms on-the-fly.
Thu, 06 Nov 2008 11:52:42 +0100 nipkow added lemma
Fri, 10 Oct 2008 06:45:53 +0200 haftmann `code func` now just `code`
Thu, 09 Oct 2008 08:47:27 +0200 haftmann established canonical argument order in SML code generators
Thu, 25 Sep 2008 09:28:03 +0200 haftmann discontinued special treatment of op = vs. eq_class.eq
Wed, 17 Sep 2008 21:27:08 +0200 wenzelm back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
Tue, 10 Jun 2008 15:30:33 +0200 haftmann rep_datatype command now takes list of constructors as input arguments
less more (0) -100 -60 tip