src/HOLCF/Sprod2.ML
changeset 1779 1155c06fa956
parent 1461 6bcb44e4d6e5
child 2033 639de962ded4
     1.1 --- a/src/HOLCF/Sprod2.ML	Fri May 31 19:47:23 1996 +0200
     1.2 +++ b/src/HOLCF/Sprod2.ML	Fri May 31 19:55:19 1996 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4          (etac (inst_sprod_po RS subst) 1)
     1.5          ]);
     1.6  
     1.7 -val less_sprod4a = (less_sprod4b RS defined_Ispair_rev);
     1.8 +bind_thm ("less_sprod4a", less_sprod4b RS defined_Ispair_rev);
     1.9  (* Ispair ?a ?b << Ispair UU UU ==> ?a = UU | ?b = UU *)
    1.10  
    1.11  qed_goal "less_sprod4c" Sprod2.thy
    1.12 @@ -252,7 +252,7 @@
    1.13          (etac (monofun_Issnd RS ub2ub_monofun) 1)
    1.14          ]);
    1.15  
    1.16 -val thelub_sprod = (lub_sprod RS thelubI);
    1.17 +bind_thm ("thelub_sprod", lub_sprod RS thelubI);
    1.18  
    1.19  
    1.20  qed_goal "cpo_sprod" Sprod2.thy