src/HOL/HOLCF/ex/Hoare.thy

--- a/src/HOL/HOLCF/ex/Hoare.thy	Sun Nov 20 21:05:23 2011 +0100
+++ b/src/HOL/HOLCF/ex/Hoare.thy	Sun Nov 20 21:07:06 2011 +0100
@@ -155,8 +155,6 @@
 
 (* -------- results about p for case (EX k. b1$(iterate k$g$x)~=TT) ------- *)
 
-thm hoare_lemma8 [THEN hoare_lemma9 [THEN mp], standard]
-
 lemma hoare_lemma10:
   "EX k. b1$(iterate k$g$x) ~= TT
     ==> Suc k = (LEAST n. b1$(iterate n$g$x) ~= TT) ==> p$(iterate k$g$x) = p$x"