--- a/src/HOL/HoareParallel/RG_Hoare.thy Mon Apr 29 11:30:15 2002 +0200
+++ b/src/HOL/HoareParallel/RG_Hoare.thy Mon Apr 29 16:45:12 2002 +0200
@@ -18,7 +18,7 @@
inductive rghoare
intros
- Basic: "\<lbrakk> pre \<subseteq> {s. f s \<in> post}; {(s,t). s \<in> pre \<and> t=f s} \<subseteq> guar;
+ Basic: "\<lbrakk> pre \<subseteq> {s. f s \<in> post}; {(s,t). s \<in> pre \<and> (t=f s \<or> t=s)} \<subseteq> guar;
stable pre rely; stable post rely \<rbrakk>
\<Longrightarrow> \<turnstile> Basic f sat [pre, rely, guar, post]"