src/HOL/IMP/Hoare.thy
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Tue, 08 Oct 2002 08:20:17 +0200 nipkow Got rid of rotates because of new simplifier
Wed, 19 Dec 2001 00:26:04 +0100 wenzelm tuned;
Sun, 09 Dec 2001 15:26:13 +0100 kleing tuned
Sun, 09 Dec 2001 14:35:36 +0100 kleing converted to Isar
Tue, 04 Jul 2000 10:54:46 +0200 oheimb disambiguated := ; added Examples (factorial)
Tue, 30 Jun 1998 20:51:15 +0200 berghofe Adapted to new inductive definition package.
Wed, 06 May 1998 11:46:00 +0200 nipkow Changed [/] to [:=] and removed actual definition.
Fri, 10 Oct 1997 19:02:28 +0200 wenzelm fixed dots;
Tue, 18 Mar 1997 18:02:19 +0100 nipkow Added wp_while.
Thu, 06 Jun 1996 14:39:44 +0200 paulson Quotes now optional around inductive set
Sat, 27 Apr 1996 18:47:31 +0200 nipkow A completely new version of IMP.
Fri, 09 Feb 1996 13:41:59 +0100 nipkow Introduced qed_spec_mp.
Wed, 07 Feb 1996 12:22:32 +0100 nipkow Modified datatype com.
Mon, 05 Feb 1996 21:29:06 +0100 clasohm expanded tabs; incorporated Konrad's changes
Tue, 23 Jan 1996 10:59:35 +0100 nipkow Added a verified verification-condition generator.
Wed, 29 Nov 1995 17:01:41 +0100 clasohm removed quotes from consts and syntax sections
Fri, 24 Mar 1995 12:30:35 +0100 clasohm changed syntax of tuples from <..., ...> to (..., ...)
Wed, 08 Mar 1995 10:25:50 +0100 nipkow Added pretty-printing coments
Tue, 07 Mar 1995 15:00:34 +0100 nipkow *** empty log message ***
Tue, 07 Mar 1995 14:59:24 +0100 nipkow *** empty log message ***
Tue, 07 Mar 1995 14:57:37 +0100 nipkow Hoare logic
less more (0) tip