| Sun, 06 May 2007 21:50:17 +0200 |
haftmann |
changed code generator invocation syntax
|
file |
diff |
annotate
|
| Thu, 26 Apr 2007 13:33:05 +0200 |
haftmann |
cleaned up code generator setup for int
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 11:21:42 +0200 |
haftmann |
Isar definitions are now added explicitly to code theorem table
|
file |
diff |
annotate
|
| Sun, 15 Apr 2007 23:25:52 +0200 |
wenzelm |
read prop as prop, not term;
|
file |
diff |
annotate
|
| Tue, 20 Mar 2007 15:52:40 +0100 |
haftmann |
added instance for lattice
|
file |
diff |
annotate
|
| Fri, 16 Mar 2007 21:32:12 +0100 |
haftmann |
added lattice definitions
|
file |
diff |
annotate
|
| Fri, 02 Mar 2007 15:43:23 +0100 |
haftmann |
tuned code theorems
|
file |
diff |
annotate
|
| Wed, 27 Dec 2006 19:10:00 +0100 |
haftmann |
added OCaml code generation (without dictionaries)
|
file |
diff |
annotate
|
| Wed, 13 Dec 2006 15:45:31 +0100 |
haftmann |
introduced mk/dest_numeral/number for mk/dest_binum etc.
|
file |
diff |
annotate
|
| Mon, 27 Nov 2006 13:42:48 +0100 |
haftmann |
small syntax tuning
|
file |
diff |
annotate
|
| Wed, 22 Nov 2006 10:20:12 +0100 |
haftmann |
dropped eq const
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 13:48:29 +0100 |
wenzelm |
removed theory NatArith (now part of Nat);
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 00:34:15 +0100 |
huffman |
generalized types of of_nat and of_int to work with non-commutative types
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 11:47:57 +0100 |
wenzelm |
renamed 'const_syntax' to 'notation';
|
file |
diff |
annotate
|
| Mon, 06 Nov 2006 16:28:31 +0100 |
haftmann |
code generator module naming improved
|
file |
diff |
annotate
|
| Tue, 31 Oct 2006 09:28:56 +0100 |
haftmann |
adapted to new serializer syntax
|
file |
diff |
annotate
|
| Fri, 20 Oct 2006 17:07:27 +0200 |
haftmann |
added reserved words for Haskell
|
file |
diff |
annotate
|
| Mon, 16 Oct 2006 14:07:31 +0200 |
haftmann |
moved HOL code generator setup to Code_Generator
|
file |
diff |
annotate
|
| Tue, 26 Sep 2006 13:34:16 +0200 |
haftmann |
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 15:21:58 +0200 |
haftmann |
improved numeral handling for nbe
|
file |
diff |
annotate
|
| Wed, 06 Sep 2006 13:48:02 +0200 |
haftmann |
got rid of Numeral.bin type
|
file |
diff |
annotate
|
| Fri, 01 Sep 2006 08:36:51 +0200 |
haftmann |
final syntax for some Isar code generator keywords
|
file |
diff |
annotate
|
| Wed, 30 Aug 2006 03:19:08 +0200 |
webertj |
lin_arith_prover: splitting reverted because of performance loss
|
file |
diff |
annotate
|
| Tue, 08 Aug 2006 08:19:44 +0200 |
haftmann |
cleanup code generation for Numerals
|
file |
diff |
annotate
|
| Sat, 29 Jul 2006 13:15:12 +0200 |
webertj |
lin_arith_prover splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 19:23:04 +0200 |
webertj |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
| Sun, 23 Jul 2006 07:21:22 +0200 |
haftmann |
fixed bug for serialization for uminus on ints
|
file |
diff |
annotate
|
| Fri, 21 Jul 2006 14:48:35 +0200 |
haftmann |
simplification for code generation for Integers
|
file |
diff |
annotate
|
| Wed, 12 Jul 2006 17:00:22 +0200 |
haftmann |
adaptions in codegen
|
file |
diff |
annotate
|
| Wed, 14 Jun 2006 12:12:37 +0200 |
haftmann |
slight refinements for code generator
|
file |
diff |
annotate
|
| Tue, 16 May 2006 21:33:01 +0200 |
wenzelm |
tuned concrete syntax -- abbreviation/const_syntax;
|
file |
diff |
annotate
|
| Tue, 09 May 2006 10:10:28 +0200 |
haftmann |
added codegen preprocessors for numerals
|
file |
diff |
annotate
|
| Tue, 02 May 2006 20:42:30 +0200 |
wenzelm |
replaced syntax/translations by abbreviation;
|
file |
diff |
annotate
|
| Thu, 06 Apr 2006 16:12:57 +0200 |
haftmann |
added explicit serialization for int equality
|
file |
diff |
annotate
|
| Fri, 17 Mar 2006 09:34:23 +0100 |
haftmann |
renamed op < <= to Orderings.less(_eq)
|
file |
diff |
annotate
|
| Fri, 10 Mar 2006 15:33:48 +0100 |
haftmann |
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
|
file |
diff |
annotate
|
| Sat, 25 Feb 2006 15:19:47 +0100 |
haftmann |
improved codegen bootstrap
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 19:01:09 +0100 |
nipkow |
got rid of superfluous linorder_neqE-instance for int.
|
file |
diff |
annotate
|
| Fri, 03 Feb 2006 08:48:16 +0100 |
haftmann |
fix in codegen
|
file |
diff |
annotate
|
| Mon, 23 Jan 2006 14:07:52 +0100 |
haftmann |
removed problematic keyword 'atom'
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
| Wed, 18 Jan 2006 11:55:50 +0100 |
haftmann |
substantial improvement in serialization handling
|
file |
diff |
annotate
|
| Tue, 17 Jan 2006 16:36:57 +0100 |
haftmann |
substantial improvements in code generator
|
file |
diff |
annotate
|
| Thu, 29 Dec 2005 15:31:10 +0100 |
haftmann |
adaptions to changes in code generator
|
file |
diff |
annotate
|
| Fri, 02 Dec 2005 16:05:12 +0100 |
haftmann |
adjusted to improved code generator interface
|
file |
diff |
annotate
|
| Tue, 22 Nov 2005 12:59:25 +0100 |
haftmann |
added codegenerator
|
file |
diff |
annotate
|
| Tue, 08 Nov 2005 09:13:22 +0100 |
haftmann |
(fix for accidental commit)
|
file |
diff |
annotate
|
| Tue, 08 Nov 2005 09:12:02 +0100 |
haftmann |
(codegen)
|
file |
diff |
annotate
|
| Tue, 27 Sep 2005 12:14:39 +0200 |
berghofe |
Inserted clause for nat in number_of_codegen again ("code unfold" turned
|
file |
diff |
annotate
|
| Wed, 21 Sep 2005 12:02:56 +0200 |
berghofe |
Simplified code generator for numerals.
|
file |
diff |
annotate
|
| Sat, 17 Sep 2005 18:11:24 +0200 |
wenzelm |
added quickcheck_params (from Main.thy);
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 18:53:11 +0200 |
paulson |
more simprules now have names
|
file |
diff |
annotate
|
| Tue, 12 Jul 2005 11:51:31 +0200 |
berghofe |
Auxiliary functions to be used in generated code are now defined using "attach".
|
file |
diff |
annotate
|
| Thu, 07 Jul 2005 12:39:17 +0200 |
nipkow |
linear arithmetic now takes "&" in assumptions apart.
|
file |
diff |
annotate
|
| Fri, 01 Jul 2005 14:08:53 +0200 |
berghofe |
Moved code generator setup from NatBin to IntDef.
|
file |
diff |
annotate
|
| Thu, 16 Jun 2005 19:51:04 +0200 |
paulson |
a few new integer lemmas
|
file |
diff |
annotate
|
| Wed, 04 May 2005 08:36:10 +0200 |
nipkow |
Fixing a problem with lin.arith.
|
file |
diff |
annotate
|
| Wed, 02 Mar 2005 10:02:21 +0100 |
paulson |
new lemmas int_diff_cases
|
file |
diff |
annotate
|
| Tue, 01 Mar 2005 18:48:52 +0100 |
nipkow |
integrated Jeremy's FiniteLib
|
file |
diff |
annotate
|