Mon, 30 Sep 2002 15:44:21 +0200 |
nipkow |
modified induct method
|
file |
diff |
annotate
|
Sun, 09 Dec 2001 15:26:13 +0100 |
kleing |
tuned
|
file |
diff |
annotate
|
Sun, 09 Dec 2001 14:35:36 +0100 |
kleing |
converted to Isar
|
file |
diff |
annotate
|
Tue, 04 Jul 2000 10:54:46 +0200 |
oheimb |
disambiguated := ; added Examples (factorial)
|
file |
diff |
annotate
|
Fri, 24 Jul 1998 13:03:20 +0200 |
berghofe |
Adapted to new datatype package.
|
file |
diff |
annotate
|
Wed, 06 May 1998 11:46:00 +0200 |
nipkow |
Changed [/] to [:=] and removed actual definition.
|
file |
diff |
annotate
|
Fri, 10 Oct 1997 19:02:28 +0200 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
Tue, 18 Mar 1997 18:02:19 +0100 |
nipkow |
Added wp_while.
|
file |
diff |
annotate
|
Thu, 08 Aug 1996 11:34:29 +0200 |
berghofe |
Simplified primrec definitions.
|
file |
diff |
annotate
|
Sat, 27 Apr 1996 18:47:31 +0200 |
nipkow |
A completely new version of IMP.
|
file |
diff |
annotate
|
Wed, 07 Feb 1996 12:22:32 +0100 |
nipkow |
Modified datatype com.
|
file |
diff |
annotate
|
Mon, 05 Feb 1996 21:29:06 +0100 |
clasohm |
expanded tabs; incorporated Konrad's changes
|
file |
diff |
annotate
|
Tue, 23 Jan 1996 14:25:55 +0100 |
nipkow |
Added vcwp
|
file |
diff |
annotate
|
Tue, 23 Jan 1996 10:59:35 +0100 |
nipkow |
Added a verified verification-condition generator.
|
file |
diff |
annotate
|