src/HOL/Lambda/WeakNorm.thy
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;
Sun, 24 Aug 2008 14:42:24 +0200 haftmann default replaces arbitrary
Wed, 02 Jul 2008 07:11:57 +0200 haftmann cleaned up some code generator configuration
Fri, 12 Oct 2007 08:21:09 +0200 haftmann consolidated naming conventions for code generator theories
Tue, 25 Sep 2007 21:08:34 +0200 haftmann Efficient_Nat and Pretty_Int integrated with ML_Int
Tue, 18 Sep 2007 16:08:00 +0200 wenzelm simplified type int (eliminated IntInf.int, integer);
Thu, 06 Sep 2007 11:44:21 +0200 berghofe Moved definition of normal forms to new NormalForm theory.
Fri, 24 Aug 2007 14:14:20 +0200 haftmann overloaded definitions accompanied by explicit constants
Mon, 20 Aug 2007 18:07:49 +0200 haftmann renamed code_gen to export_code
Mon, 13 Aug 2007 21:22:37 +0200 haftmann renamed keyword "to" to "module_name"
Fri, 10 Aug 2007 17:04:34 +0200 haftmann new structure for code generator modules
Mon, 16 Jul 2007 09:29:03 +0200 haftmann dropped outer ROOT structure for generated code
Wed, 11 Jul 2007 11:23:24 +0200 berghofe - Renamed inductive2 to inductive
Thu, 21 Jun 2007 20:07:26 +0200 wenzelm tuned proofs -- avoid implicit prems;
Fri, 15 Jun 2007 19:19:23 +0200 berghofe Locally added definition of "int :: nat => int" again to make
Thu, 10 May 2007 15:51:59 +0200 berghofe Moved extraction_expand declaration of listall_def outside of definition.
Thu, 10 May 2007 10:22:17 +0200 haftmann consts in consts_code Isar commands are now referred to by usual term syntax
Sun, 06 May 2007 21:50:17 +0200 haftmann changed code generator invocation syntax
Thu, 26 Apr 2007 13:32:59 +0200 haftmann moved code generation pretty integers and characters to separate theories
Fri, 23 Mar 2007 12:06:41 +0100 haftmann fixed typing bug in generated code
Fri, 23 Mar 2007 12:05:43 +0100 haftmann fixed typing bug in generated code
Thu, 22 Mar 2007 14:03:30 +0100 haftmann fixed code generator setup
Wed, 07 Feb 2007 17:44:07 +0100 berghofe Adapted to new inductive definition package.
Mon, 27 Nov 2006 13:42:33 +0100 haftmann removed HOL structure
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Mon, 13 Nov 2006 15:43:12 +0100 haftmann adjusted name in generated code
Tue, 07 Nov 2006 11:47:57 +0100 wenzelm renamed 'const_syntax' to 'notation';
Mon, 06 Nov 2006 16:28:37 +0100 haftmann (adjustions)
Tue, 31 Oct 2006 14:58:12 +0100 haftmann adapted to new serializer syntax
Fri, 13 Oct 2006 16:52:46 +0200 haftmann added codegen2 example
Tue, 10 Oct 2006 10:34:42 +0200 haftmann purged some ML legacy
Mon, 02 Oct 2006 23:00:56 +0200 haftmann cleaned mess
Tue, 26 Sep 2006 13:34:16 +0200 haftmann renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
Mon, 11 Sep 2006 21:35:19 +0200 wenzelm induct method: renamed 'fixing' to 'arbitrary';
Fri, 01 Sep 2006 08:36:51 +0200 haftmann final syntax for some Isar code generator keywords
Wed, 14 Jun 2006 12:14:42 +0200 haftmann slight adaption for code generator
Tue, 06 Jun 2006 15:02:09 +0200 haftmann added arbitray setup for codegen 2
Tue, 16 May 2006 21:33:01 +0200 wenzelm tuned concrete syntax -- abbreviation/const_syntax;
Sun, 09 Apr 2006 18:51:13 +0200 wenzelm tuned syntax/abbreviations;
Sat, 08 Apr 2006 22:51:06 +0200 wenzelm refined 'abbreviation';
Thu, 16 Feb 2006 21:12:00 +0100 wenzelm new-style definitions/abbreviations;
Fri, 23 Dec 2005 20:02:30 +0100 wenzelm tuned proofs;
Fri, 02 Dec 2005 13:10:12 +0100 berghofe Factored out proof for normalization of applications (norm_list).
Fri, 25 Nov 2005 19:09:44 +0100 wenzelm tuned induct proofs;
Wed, 23 Nov 2005 22:26:13 +0100 wenzelm tuned induction proofs;
Thu, 22 Sep 2005 23:56:15 +0200 nipkow renamed rules to iprover
Thu, 25 Aug 2005 16:13:09 +0200 berghofe Adapted to new code generator syntax.
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Tue, 10 May 2005 10:25:21 +0200 paulson oops...cannot use subst here
Mon, 09 May 2005 16:38:56 +0200 paulson from simplesubst to new subst
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Wed, 02 Feb 2005 18:20:31 +0100 berghofe Replaced application of subst by simplesubst in proof of app_Var_NF
Mon, 11 Oct 2004 07:42:22 +0200 nipkow Proofs needed to be updated because induction now preserves name of
Tue, 01 Jun 2004 15:00:26 +0200 berghofe Adapted to new name mangling function in code generator.
Tue, 24 Jun 2003 10:37:12 +0200 berghofe New proof of weak normalization with program extraction.
less more (0) tip