src/HOLCF/Cfun2.ML
changeset 1989 8e0ff1bfcfea
parent 1779 1155c06fa956
child 2033 639de962ded4
     1.1 --- a/src/HOLCF/Cfun2.ML	Thu Sep 12 15:22:52 1996 +0200
     1.2 +++ b/src/HOLCF/Cfun2.ML	Thu Sep 12 17:18:00 1996 +0200
     1.3 @@ -111,6 +111,13 @@
     1.4          ]);
     1.5  
     1.6  
     1.7 +qed_goal "strictI" Cfun2.thy "f`x = UU ==> f`UU = UU" (fn prems => [
     1.8 +	cut_facts_tac prems 1,
     1.9 +	rtac (eq_UU_iff RS iffD2) 1,
    1.10 +	etac subst 1,
    1.11 +	rtac (minimal RS monofun_cfun_arg) 1]);
    1.12 +
    1.13 +
    1.14  (* ------------------------------------------------------------------------ *)
    1.15  (* ch2ch - rules for the type 'a -> 'b                                      *)
    1.16  (* use MF2 lemmas from Cont.ML                                              *)