src/HOLCF/Cfun2.ML
changeset 1779 1155c06fa956
parent 1461 6bcb44e4d6e5
child 1989 8e0ff1bfcfea
     1.1 --- a/src/HOLCF/Cfun2.ML	Fri May 31 19:47:23 1996 +0200
     1.2 +++ b/src/HOLCF/Cfun2.ML	Fri May 31 19:55:19 1996 +0200
     1.3 @@ -48,11 +48,11 @@
     1.4          (rtac Rep_Cfun 1)
     1.5          ]);
     1.6  
     1.7 -val monofun_fapp2 = cont_fapp2 RS cont2mono;
     1.8 +bind_thm ("monofun_fapp2", cont_fapp2 RS cont2mono);
     1.9  (* monofun(fapp(?fo1)) *)
    1.10  
    1.11  
    1.12 -val contlub_fapp2 = cont_fapp2 RS cont2contlub;
    1.13 +bind_thm ("contlub_fapp2", cont_fapp2 RS cont2contlub);
    1.14  (* contlub(fapp(?fo1)) *)
    1.15  
    1.16  (* ------------------------------------------------------------------------ *)
    1.17 @@ -60,10 +60,10 @@
    1.18  (* looks nice with mixfix syntac                                            *)
    1.19  (* ------------------------------------------------------------------------ *)
    1.20  
    1.21 -val cont_cfun_arg = (cont_fapp2 RS contE RS spec RS mp);
    1.22 +bind_thm ("cont_cfun_arg", (cont_fapp2 RS contE RS spec RS mp));
    1.23  (* is_chain(?x1) ==> range (%i. ?fo3`(?x1 i)) <<| ?fo3`(lub (range ?x1))    *)
    1.24   
    1.25 -val contlub_cfun_arg = (contlub_fapp2 RS contlubE RS spec RS mp);
    1.26 +bind_thm ("contlub_cfun_arg", (contlub_fapp2 RS contlubE RS spec RS mp));
    1.27  (* is_chain(?x1) ==> ?fo4`(lub (range ?x1)) = lub (range (%i. ?fo4`(?x1 i))) *)
    1.28  
    1.29  
    1.30 @@ -93,7 +93,7 @@
    1.31          ]);
    1.32  
    1.33  
    1.34 -val monofun_cfun_arg = (monofun_fapp2 RS monofunE RS spec RS spec RS mp);
    1.35 +bind_thm ("monofun_cfun_arg", monofun_fapp2 RS monofunE RS spec RS spec RS mp);
    1.36  (* ?x2 << ?x1 ==> ?fo5`?x2 << ?fo5`?x1                                      *)
    1.37  
    1.38  (* ------------------------------------------------------------------------ *)
    1.39 @@ -125,7 +125,7 @@
    1.40          ]);
    1.41  
    1.42  
    1.43 -val ch2ch_fappL = (monofun_fapp1 RS ch2ch_MF2L);
    1.44 +bind_thm ("ch2ch_fappL", monofun_fapp1 RS ch2ch_MF2L);
    1.45  (* is_chain(?F) ==> is_chain (%i. ?F i`?x)                                  *)
    1.46  
    1.47  
    1.48 @@ -210,7 +210,7 @@
    1.49          (etac (monofun_fapp1 RS ub2ub_monofun) 1)
    1.50          ]);
    1.51  
    1.52 -val thelub_cfun = (lub_cfun RS thelubI);
    1.53 +bind_thm ("thelub_cfun", lub_cfun RS thelubI);
    1.54  (* 
    1.55  is_chain(?CCF1) ==>  lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x)))
    1.56  *)