| 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
|
| Mon, 21 Feb 2005 15:57:45 +0100 |
nipkow |
removed superfluous setsum_constant
|
file |
diff |
annotate
|
| Mon, 21 Feb 2005 15:04:10 +0100 |
nipkow |
comprehensive cleanup, replacing sumr by setsum
|
file |
diff |
annotate
|
| Tue, 01 Feb 2005 18:01:57 +0100 |
paulson |
the new subst tactic, by Lucas Dixon
|
file |
diff |
annotate
|