| Fri, 10 Oct 2008 06:45:53 +0200 |
`code func` now just `code`
|
file | diff | annotate |
| Thu, 09 Oct 2008 08:47:27 +0200 |
established canonical argument order in SML code generators
|
file | diff | annotate |
| Thu, 25 Sep 2008 09:28:03 +0200 |
discontinued special treatment of op = vs. eq_class.eq
|
file | diff | annotate |
| Wed, 17 Sep 2008 21:27:08 +0200 |
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
|
file | diff | annotate |
| Tue, 10 Jun 2008 15:30:33 +0200 |
rep_datatype command now takes list of constructors as input arguments
|
file | diff | annotate |
| Fri, 23 May 2008 16:41:39 +0200 |
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
|
file | diff | annotate |
| Wed, 07 May 2008 10:56:40 +0200 |
split_beta is now declared as monotonicity rule, to allow bounded
|
file | diff | annotate |
| Wed, 09 Apr 2008 08:10:11 +0200 |
removed syntax from monad combinators; renamed mbind to scomp
|
file | diff | annotate |
| Sat, 29 Mar 2008 19:14:00 +0100 |
replaced 'ML_setup' by 'ML';
|
file | diff | annotate |
| Thu, 20 Mar 2008 12:04:54 +0100 |
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
|
file | diff | annotate |
| Wed, 19 Mar 2008 22:47:38 +0100 |
more antiquotations;
|
file | diff | annotate |
| Tue, 26 Feb 2008 11:18:43 +0100 |
Added useful general lemmas from the work with the HeapMonad
|
file | diff | annotate |
| Thu, 10 Jan 2008 19:09:21 +0100 |
New interface for test data generators.
|
file | diff | annotate |
| Wed, 05 Dec 2007 14:15:45 +0100 |
simplified infrastructure for code generator operational equality
|
file | diff | annotate |
| Fri, 30 Nov 2007 20:13:05 +0100 |
more canonical attribute application
|
file | diff | annotate |
| Thu, 04 Oct 2007 19:54:44 +0200 |
certificates for code generator case expressions
|
file | diff | annotate |
| Tue, 25 Sep 2007 12:16:08 +0200 |
datatype interpretators for size and datatype_realizer
|
file | diff | annotate |
| Wed, 15 Aug 2007 12:52:56 +0200 |
ATP blacklisting is now in theory data, attribute noatp
|
file | diff | annotate |
| Tue, 07 Aug 2007 09:38:44 +0200 |
split off theory Option for benefit of code generator
|
file | diff | annotate |
| Tue, 05 Jun 2007 15:16:08 +0200 |
merged Code_Generator.thy into HOL.thy
|
file | diff | annotate |
| Wed, 09 May 2007 07:53:06 +0200 |
moved recfun_codegen.ML to Code_Generator.thy
|
file | diff | annotate |
| Sun, 06 May 2007 21:49:23 +0200 |
tuned
|
file | diff | annotate |
| Fri, 20 Apr 2007 11:21:42 +0200 |
Isar definitions are now added explicitly to code theorem table
|
file | diff | annotate |
| Wed, 04 Apr 2007 00:10:59 +0200 |
ML antiquotes;
|
file | diff | annotate |
| Mon, 12 Mar 2007 19:23:49 +0100 |
syntax: proper body priorty for derived binders;
|
file | diff | annotate |
| Fri, 02 Mar 2007 15:43:20 +0100 |
using "fst" "snd" for Haskell code
|
file | diff | annotate |
| Fri, 23 Feb 2007 08:39:22 +0100 |
slight cleanup
|
file | diff | annotate |
| Wed, 27 Dec 2006 19:09:57 +0100 |
moved code generator product setup here
|
file | diff | annotate |
| Wed, 22 Nov 2006 10:20:12 +0100 |
dropped eq const
|
file | diff | annotate |
| Fri, 17 Nov 2006 02:20:03 +0100 |
more robust syntax for definition/abbreviation/notation;
|
file | diff | annotate |
| Mon, 13 Nov 2006 15:43:08 +0100 |
added thy dependencies
|
file | diff | annotate |
| Tue, 07 Nov 2006 11:47:57 +0100 |
renamed 'const_syntax' to 'notation';
|
file | diff | annotate |
| Mon, 06 Nov 2006 16:28:36 +0100 |
two further lemmas on split
|
file | diff | annotate |
| Mon, 16 Oct 2006 14:07:31 +0200 |
moved HOL code generator setup to Code_Generator
|
file | diff | annotate |
| Tue, 19 Sep 2006 15:21:42 +0200 |
added operational equality
|
file | diff | annotate |
| Fri, 25 Aug 2006 18:45:57 +0200 |
explicit type variables prevent empty sorts
|
file | diff | annotate |
| Mon, 14 Aug 2006 13:46:06 +0200 |
simplified code generator setup
|
file | diff | annotate |
| Wed, 12 Jul 2006 17:00:22 +0200 |
adaptions in codegen
|
file | diff | annotate |
| Sat, 08 Jul 2006 12:54:30 +0200 |
simprocs: no theory argument -- use simpset context instead;
|
file | diff | annotate |
| Tue, 16 May 2006 21:33:01 +0200 |
tuned concrete syntax -- abbreviation/const_syntax;
|
file | diff | annotate |
| Tue, 02 May 2006 20:42:30 +0200 |
replaced syntax/translations by abbreviation;
|
file | diff | annotate |
| Fri, 03 Mar 2006 19:30:20 +0100 |
changed and retracted change of location of code lemmas.
|
file | diff | annotate |
| Sat, 25 Feb 2006 15:19:47 +0100 |
improved codegen bootstrap
|
file | diff | annotate |
| Mon, 20 Feb 2006 11:38:06 +0100 |
slight code generator serialization improvements
|
file | diff | annotate |
| Tue, 14 Feb 2006 17:07:48 +0100 |
added theory of executable rational numbers
|
file | diff | annotate |
| Fri, 10 Feb 2006 09:09:07 +0100 |
improved code generator devarification
|
file | diff | annotate |
| Tue, 07 Feb 2006 08:47:43 +0100 |
slight improvements in code generation
|
file | diff | annotate |
| Mon, 23 Jan 2006 14:07:52 +0100 |
removed problematic keyword 'atom'
|
file | diff | annotate |
| Thu, 19 Jan 2006 21:22:08 +0100 |
setup: theory -> theory;
|
file | diff | annotate |
| Thu, 19 Jan 2006 14:59:55 +0100 |
Re-inserted consts_code declaration accidentally deleted
|
file | diff | annotate |
| Tue, 17 Jan 2006 16:36:57 +0100 |
substantial improvements in code generator
|
file | diff | annotate |
| Thu, 29 Dec 2005 15:31:10 +0100 |
adaptions to changes in code generator
|
file | diff | annotate |
| Thu, 08 Dec 2005 20:15:50 +0100 |
tuned proofs;
|
file | diff | annotate |
| Fri, 02 Dec 2005 16:05:12 +0100 |
adjusted to improved code generator interface
|
file | diff | annotate |
| Thu, 01 Dec 2005 22:04:27 +0100 |
simprocs: static evaluation of simpset;
|
file | diff | annotate |
| Tue, 22 Nov 2005 12:59:25 +0100 |
added codegenerator
|
file | diff | annotate |
| Fri, 28 Oct 2005 17:27:04 +0200 |
added extraction interface for code generator
|
file | diff | annotate |
| Fri, 21 Oct 2005 18:14:34 +0200 |
Goal.prove;
|
file | diff | annotate |
| Mon, 17 Oct 2005 23:10:10 +0200 |
change_claset/simpset;
|
file | diff | annotate |
| Fri, 07 Oct 2005 22:59:19 +0200 |
replaced _K by dummy abstraction;
|
file | diff | annotate |