src/HOL/HoareParallel/RG_Hoare.thy
Wed, 11 Jul 2007 11:14:51 +0200 berghofe Adapted to new inductive definition package.
Wed, 30 Aug 2006 03:19:08 +0200 webertj lin_arith_prover: splitting reverted because of performance loss
Mon, 31 Jul 2006 21:06:40 +0200 webertj lin_arith_prover splits certain operators (e.g. min, max, abs)
Wed, 26 Jul 2006 19:23:04 +0200 webertj linear arithmetic splits certain operators (e.g. min, max, abs)
Wed, 04 Jan 2006 19:22:53 +0100 nipkow Reversed Larry's option/iff change.
Wed, 21 Dec 2005 12:02:57 +0100 paulson removed or modified some instances of [iff]
Thu, 22 Sep 2005 23:55:42 +0200 nipkow fix because of list lemmas
Thu, 22 Sep 2005 14:02:14 +0200 nipkow Fix because of new lemma in List
Tue, 20 Sep 2005 20:16:55 +0200 wenzelm fixed proof script of lemma Cond_sound (Why did it stop working anyway?);
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Mon, 11 Oct 2004 07:42:22 +0200 nipkow Proofs needed to be updated because induction now preserves name of
Tue, 03 Aug 2004 13:48:00 +0200 paulson new simprules Int_subset_iff and Un_subset_iff
Mon, 22 Dec 2003 22:52:38 +0100 nipkow Updated proofs due to changes in Set.thy.
Wed, 14 May 2003 10:22:09 +0200 nipkow *** empty log message ***
Mon, 30 Sep 2002 16:14:02 +0200 berghofe Adapted to new simplifier.
Tue, 27 Aug 2002 11:03:05 +0200 wenzelm *** empty log message ***
Thu, 30 May 2002 10:12:52 +0200 nipkow Modifications due to enhanced linear arithmetic.
Mon, 29 Apr 2002 16:45:12 +0200 prensani added abstract;corrected RG_Basic Hoare rule.
Tue, 05 Mar 2002 18:19:11 +0100 prensani New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
Tue, 05 Mar 2002 17:11:25 +0100 prensani HoareParallel Theories
less more (0) tip