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