| Wed, 23 Apr 1997 11:18:29 +0200 | paulson | Ran expandshort | file | diff | annotate |
| Wed, 02 Apr 1997 11:30:48 +0200 | paulson | Replaced Best_tac by the one rule needed for the proof | file | diff | annotate |
| Tue, 18 Mar 1997 18:02:19 +0100 | nipkow | Added wp_while. | file | diff | annotate |
| Mon, 07 Oct 1996 10:26:00 +0200 | paulson | Ran expandshort | file | diff | annotate |
| Thu, 26 Sep 1996 12:47:47 +0200 | paulson | Ran expandshort | file | diff | annotate |
| Tue, 10 Sep 1996 20:10:29 +0200 | nipkow | Converted proofs to use default clasets. | file | diff | annotate |
| 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 |