src/HOL/Product_Type.thy
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
Fri, 23 May 2008 16:41:39 +0200 berghofe Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
Wed, 07 May 2008 10:56:40 +0200 berghofe split_beta is now declared as monotonicity rule, to allow bounded
Wed, 09 Apr 2008 08:10:11 +0200 haftmann removed syntax from monad combinators; renamed mbind to scomp
Sat, 29 Mar 2008 19:14:00 +0100 wenzelm replaced 'ML_setup' by 'ML';
Thu, 20 Mar 2008 12:04:54 +0100 haftmann Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
Wed, 19 Mar 2008 22:47:38 +0100 wenzelm more antiquotations;
Tue, 26 Feb 2008 11:18:43 +0100 bulwahn Added useful general lemmas from the work with the HeapMonad
Thu, 10 Jan 2008 19:09:21 +0100 berghofe New interface for test data generators.
Wed, 05 Dec 2007 14:15:45 +0100 haftmann simplified infrastructure for code generator operational equality
Fri, 30 Nov 2007 20:13:05 +0100 haftmann more canonical attribute application
Thu, 04 Oct 2007 19:54:44 +0200 haftmann certificates for code generator case expressions
Tue, 25 Sep 2007 12:16:08 +0200 haftmann datatype interpretators for size and datatype_realizer
Wed, 15 Aug 2007 12:52:56 +0200 paulson ATP blacklisting is now in theory data, attribute noatp
Tue, 07 Aug 2007 09:38:44 +0200 haftmann split off theory Option for benefit of code generator
Tue, 05 Jun 2007 15:16:08 +0200 haftmann merged Code_Generator.thy into HOL.thy
Wed, 09 May 2007 07:53:06 +0200 haftmann moved recfun_codegen.ML to Code_Generator.thy
Sun, 06 May 2007 21:49:23 +0200 haftmann tuned
Fri, 20 Apr 2007 11:21:42 +0200 haftmann Isar definitions are now added explicitly to code theorem table
Wed, 04 Apr 2007 00:10:59 +0200 wenzelm ML antiquotes;
Mon, 12 Mar 2007 19:23:49 +0100 wenzelm syntax: proper body priorty for derived binders;
Fri, 02 Mar 2007 15:43:20 +0100 haftmann using "fst" "snd" for Haskell code
Fri, 23 Feb 2007 08:39:22 +0100 haftmann slight cleanup
Wed, 27 Dec 2006 19:09:57 +0100 haftmann moved code generator product setup here
Wed, 22 Nov 2006 10:20:12 +0100 haftmann dropped eq const
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Mon, 13 Nov 2006 15:43:08 +0100 haftmann added thy dependencies
Tue, 07 Nov 2006 11:47:57 +0100 wenzelm renamed 'const_syntax' to 'notation';
Mon, 06 Nov 2006 16:28:36 +0100 haftmann two further lemmas on split
Mon, 16 Oct 2006 14:07:31 +0200 haftmann moved HOL code generator setup to Code_Generator
Tue, 19 Sep 2006 15:21:42 +0200 haftmann added operational equality
Fri, 25 Aug 2006 18:45:57 +0200 paulson explicit type variables prevent empty sorts
Mon, 14 Aug 2006 13:46:06 +0200 haftmann simplified code generator setup
Wed, 12 Jul 2006 17:00:22 +0200 haftmann adaptions in codegen
Sat, 08 Jul 2006 12:54:30 +0200 wenzelm simprocs: no theory argument -- use simpset context instead;
less more (0) -100 -60 tip