| changeset 1274 | ea0668a1c0ba |
| parent 1267 | bca91b4e1710 |
| child 1461 | 6bcb44e4d6e5 |
--- a/src/HOLCF/ex/Hoare.ML Fri Oct 06 16:17:08 1995 +0100 +++ b/src/HOLCF/ex/Hoare.ML Fri Oct 06 17:25:24 1995 +0100 @@ -137,8 +137,6 @@ (** --------- proves about iterations of p and q ---------- **) -val HOLCF_ss = simpset_of "HOLCF"; - val hoare_lemma9 = prove_goal Hoare.thy "(! m. m< Suc k --> b1`(iterate m g x)=TT) -->\ \ p`(iterate k g x)=p`x"