changeset 26936 | faf8a5b5ba87 |
parent 26334 | 80ec6cf82d95 |
child 35174 | e15040ae75d7 |
--- a/src/HOLCF/ex/Hoare.thy Sat May 17 23:37:09 2008 +0200 +++ b/src/HOLCF/ex/Hoare.thy Sat May 17 23:37:11 2008 +0200 @@ -158,7 +158,7 @@ (* -------- results about p for case (EX k. b1$(iterate k$g$x)~=TT) ------- *) -thm hoare_lemma8 [THEN hoare_lemma9 [THEN mp], standard, no_vars] +thm hoare_lemma8 [THEN hoare_lemma9 [THEN mp], standard] lemma hoare_lemma10: "EX k. b1$(iterate k$g$x) ~= TT