| Mon, 19 Aug 1996 11:17:20 +0200 |
paulson |
Tidied some proofs, maybe using less_SucE
|
file |
diff |
annotate
|
| Fri, 17 May 1996 12:24:47 +0200 |
nipkow |
Had to rename params because variable names in an induction rule changed.
|
file |
diff |
annotate
|
| Tue, 07 May 1996 18:19:13 +0200 |
paulson |
Updated for new form of induction rules
|
file |
diff |
annotate
|
| Sat, 27 Apr 1996 18:47:31 +0200 |
nipkow |
A completely new version of IMP.
|
file |
diff |
annotate
|
| Fri, 09 Feb 1996 13:41:59 +0100 |
nipkow |
Introduced qed_spec_mp.
|
file |
diff |
annotate
|
| Wed, 07 Feb 1996 12:22:32 +0100 |
nipkow |
Modified datatype com.
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 15:24:36 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Tue, 23 Jan 1996 10:59:35 +0100 |
nipkow |
Added a verified verification-condition generator.
|
file |
diff |
annotate
|
| Wed, 04 Oct 1995 13:12:14 +0100 |
clasohm |
added local simpsets
|
file |
diff |
annotate
|
| Tue, 09 May 1995 22:10:48 +0200 |
nipkow |
Moved induct2 from Hoare to Lfp.
|
file |
diff |
annotate
|
| Fri, 24 Mar 1995 12:30:35 +0100 |
clasohm |
changed syntax of tuples from <..., ...> to (..., ...)
|
file |
diff |
annotate
|
| Tue, 07 Mar 1995 15:00:34 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Tue, 07 Mar 1995 14:57:37 +0100 |
nipkow |
Hoare logic
|
file |
diff |
annotate
|