| Tue, 07 Nov 2006 18:25:48 +0100 |
schirmer |
field-update in records is generalised to take a function on the field
|
file |
diff |
annotate
|
| Wed, 30 Aug 2006 03:19:08 +0200 |
webertj |
lin_arith_prover: splitting reverted because of performance loss
|
file |
diff |
annotate
|
| Mon, 31 Jul 2006 21:06:40 +0200 |
webertj |
lin_arith_prover splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
| Wed, 16 Nov 2005 19:34:19 +0100 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Mon, 02 May 2005 19:00:05 +0200 |
nipkow |
fixed
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 09:22:35 +0100 |
nipkow |
fixed proof
|
file |
diff |
annotate
|
| Thu, 15 Jul 2004 15:39:51 +0200 |
nipkow |
more summation syntax
|
file |
diff |
annotate
|
| Wed, 07 Aug 2002 18:32:50 +0200 |
nipkow |
Added time example at the end.
|
file |
diff |
annotate
|
| Sat, 06 Oct 2001 00:02:46 +0200 |
wenzelm |
* sane numerals (stage 2): plain "num" syntax (removed "#");
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:52:39 +0200 |
wenzelm |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file |
diff |
annotate
|
| Wed, 10 Jan 2001 00:15:33 +0100 |
wenzelm |
use \<acute>;
|
file |
diff |
annotate
|
| Tue, 03 Oct 2000 22:39:49 +0200 |
wenzelm |
Hoare logic in Isar;
|
file |
diff |
annotate
|