--- a/src/HOLCF/ex/Hoare.thy Wed Mar 19 18:10:23 2008 +0100
+++ b/src/HOLCF/ex/Hoare.thy Wed Mar 19 18:15:13 2008 +0100
@@ -84,11 +84,11 @@
apply (intro strip)
apply (rule_tac p = "b1$ (iterate m$g$x) " in trE)
prefer 2 apply (assumption)
-apply (rule le_less_trans [THEN less_irrefl])
+apply (rule le_less_trans [THEN less_irrefl [THEN notE]])
prefer 2 apply (assumption)
apply (rule Least_le)
apply (erule hoare_lemma6)
-apply (rule le_less_trans [THEN less_irrefl])
+apply (rule le_less_trans [THEN less_irrefl [THEN notE]])
prefer 2 apply (assumption)
apply (rule Least_le)
apply (erule hoare_lemma7)