| changeset 40002 | c5b5f7a3a3b1 |
| parent 35948 | 5e7909f0346b |
| child 40028 | 9ee4e0ab2964 |
--- a/src/HOLCF/ex/Hoare.thy Mon Oct 11 16:24:44 2010 -0700 +++ b/src/HOLCF/ex/Hoare.thy Mon Oct 11 21:35:31 2010 -0700 @@ -417,7 +417,7 @@ (* ------ the main proof q o p = q ------ *) theorem hoare_main: "q oo p = q" -apply (rule ext_cfun) +apply (rule cfun_eqI) apply (subst cfcomp2) apply (rule hoare_lemma3 [THEN disjE]) apply (erule hoare_lemma23)