| Sat, 29 Nov 2008 13:39:45 +0100 |
nipkow |
Floats for Real.
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Tue, 07 Oct 2008 16:07:25 +0200 |
haftmann |
tuned code setup
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 10:17:22 +0200 |
haftmann |
non left-linear equations for nbe
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 21:31:28 +0200 |
nipkow |
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
|
file |
diff |
annotate
|
| Tue, 26 Aug 2008 12:07:06 +0200 |
nipkow |
Defined rationals (Rats) globally in Rational.
|
file |
diff |
annotate
|
| Sat, 23 Aug 2008 21:06:32 +0200 |
nipkow |
added const Rational
|
file |
diff |
annotate
|
| Mon, 11 Aug 2008 22:25:45 +0200 |
haftmann |
rudimentary code setup for set operations
|
file |
diff |
annotate
|
| Fri, 25 Jul 2008 12:03:34 +0200 |
haftmann |
added class preorder
|
file |
diff |
annotate
|
| Mon, 21 Jul 2008 13:36:59 +0200 |
chaieb |
Tuned and simplified proofs
|
file |
diff |
annotate
|
| Fri, 18 Jul 2008 18:25:56 +0200 |
haftmann |
refined code generator setup for rational numbers; more simplification rules for rational numbers
|
file |
diff |
annotate
|
| Fri, 11 Jul 2008 09:02:27 +0200 |
haftmann |
improved code generator setup
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 15:30:56 +0200 |
haftmann |
removed some dubious code lemmas
|
file |
diff |
annotate
|
| Tue, 22 Apr 2008 08:33:16 +0200 |
haftmann |
constant HOL.eq now qualified
|
file |
diff |
annotate
|
| Wed, 02 Apr 2008 15:58:32 +0200 |
haftmann |
explicit class "eq" for operational equality
|
file |
diff |
annotate
|
| Fri, 25 Jan 2008 14:54:41 +0100 |
haftmann |
improved code theorem setup
|
file |
diff |
annotate
|