src/HOLCF/ex/Hoare.thy

--- a/src/HOLCF/ex/Hoare.thy	Wed Nov 03 07:02:09 2010 -0700
+++ b/src/HOLCF/ex/Hoare.thy	Wed Nov 03 15:03:16 2010 -0700
@@ -95,9 +95,7 @@
 
 
 lemma hoare_lemma28: "f$(y::'a)=(UU::tr) ==> f$UU = UU"
-apply (erule flat_codom [THEN disjE])
-apply auto
-done
+by (rule strictI)
 
 
 (* ----- access to definitions ----- *)