src/HOLCF/Sprod2.ML
changeset 4721 c8a8482a8124
parent 4031 42cbf6256d60
child 7499 23e090051cb8
     1.1 --- a/src/HOLCF/Sprod2.ML	Tue Mar 10 18:32:37 1998 +0100
     1.2 +++ b/src/HOLCF/Sprod2.ML	Tue Mar 10 18:33:13 1998 +0100
     1.3 @@ -95,7 +95,7 @@
     1.4  (* ------------------------------------------------------------------------ *)
     1.5  
     1.6  qed_goal "lub_sprod" Sprod2.thy 
     1.7 -"[|is_chain(S)|] ==> range(S) <<| \
     1.8 +"[|chain(S)|] ==> range(S) <<| \
     1.9  \ Ispair (lub(range(%i. Isfst(S i)))) (lub(range(%i. Issnd(S i))))"
    1.10  (fn prems =>
    1.11          [
    1.12 @@ -123,7 +123,7 @@
    1.13  
    1.14  
    1.15  qed_goal "cpo_sprod" Sprod2.thy 
    1.16 -        "is_chain(S::nat=>'a**'b)==>? x. range(S)<<| x"
    1.17 +        "chain(S::nat=>'a**'b)==>? x. range(S)<<| x"
    1.18  (fn prems =>
    1.19          [
    1.20          (cut_facts_tac prems 1),