| Sat, 28 Apr 2012 07:38:22 +0200 | nipkow | renamed Semi to Seq | file | diff | annotate |
| Thu, 20 Oct 2011 09:48:00 +0200 | nipkow | renamed name -> vname | file | diff | annotate |
| Mon, 06 Jun 2011 16:29:38 +0200 | kleing | imported rest of new IMP | file | diff | annotate |
| Wed, 30 Mar 2011 23:26:40 +0200 | wenzelm | modernized specifications; | file | diff | annotate |
| Sun, 16 Jan 2011 15:53:03 +0100 | wenzelm | tuned headers; | file | diff | annotate |
| Fri, 12 Mar 2010 18:42:56 +0100 | nipkow | Reorganized Hoare logic theories; added Hoare_Den | file | diff | annotate |
| Thu, 11 Mar 2010 19:05:46 +0100 | nipkow | converted proofs to Isar | file | diff | annotate |
| Wed, 25 Jun 2008 22:01:34 +0200 | wenzelm | modernized specifications; | file | diff | annotate |
| Wed, 11 Jul 2007 11:14:51 +0200 | berghofe | Adapted to new inductive definition package. | file | diff | annotate |
| Mon, 11 Sep 2006 21:35:19 +0200 | wenzelm | induct method: renamed 'fixing' to 'arbitrary'; | file | diff | annotate |
| Thu, 08 Dec 2005 20:15:50 +0100 | wenzelm | tuned proofs; | file | diff | annotate |
| Fri, 17 Jun 2005 16:12:49 +0200 | haftmann | migrated theory headers to new format | file | diff | annotate |
| Tue, 08 Oct 2002 08:20:17 +0200 | nipkow | Got rid of rotates because of new simplifier | file | diff | annotate |
| Wed, 19 Dec 2001 00:26:04 +0100 | wenzelm | tuned; | 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 |
| Tue, 30 Jun 1998 20:51:15 +0200 | berghofe | Adapted to new inductive definition 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, 06 Jun 1996 14:39:44 +0200 | paulson | Quotes now optional around inductive set | 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 |
| Mon, 05 Feb 1996 21:29:06 +0100 | clasohm | expanded tabs; incorporated Konrad's changes | file | diff | annotate |
| Tue, 23 Jan 1996 10:59:35 +0100 | nipkow | Added a verified verification-condition generator. | file | diff | annotate |
| Wed, 29 Nov 1995 17:01:41 +0100 | clasohm | removed quotes from consts and syntax sections | file | diff | annotate |
| Fri, 24 Mar 1995 12:30:35 +0100 | clasohm | changed syntax of tuples from <..., ...> to (..., ...) | file | diff | annotate |
| Wed, 08 Mar 1995 10:25:50 +0100 | nipkow | Added pretty-printing coments | file | diff | annotate |
| Tue, 07 Mar 1995 15:00:34 +0100 | nipkow | *** empty log message *** | file | diff | annotate |
| Tue, 07 Mar 1995 14:59:24 +0100 | nipkow | *** empty log message *** | file | diff | annotate |
| Tue, 07 Mar 1995 14:57:37 +0100 | nipkow | Hoare logic | file | diff | annotate |