1.1 --- a/src/HOLCF/Cfun2.ML	Tue Mar 10 18:32:37 1998 +0100
     1.2 +++ b/src/HOLCF/Cfun2.ML	Tue Mar 10 18:33:13 1998 +0100
     1.3 @@ -75,10 +75,10 @@
     1.4  (* ------------------------------------------------------------------------ *)
     1.5  
     1.6  bind_thm ("cont_cfun_arg", (cont_fapp2 RS contE RS spec RS mp));
     1.7 -(* is_chain(?x1) ==> range (%i. ?fo3`(?x1 i)) <<| ?fo3`(lub (range ?x1))    *)
     1.8 +(* chain(?x1) ==> range (%i. ?fo3`(?x1 i)) <<| ?fo3`(lub (range ?x1))    *)
     1.9   
    1.10  bind_thm ("contlub_cfun_arg", (contlub_fapp2 RS contlubE RS spec RS mp));
    1.11 -(* is_chain(?x1) ==> ?fo4`(lub (range ?x1)) = lub (range (%i. ?fo4`(?x1 i))) *)
    1.12 +(* chain(?x1) ==> ?fo4`(lub (range ?x1)) = lub (range (%i. ?fo4`(?x1 i))) *)
    1.13  
    1.14  
    1.15  (* ------------------------------------------------------------------------ *)
    1.16 @@ -138,7 +138,7 @@
    1.17  (* ------------------------------------------------------------------------ *)
    1.18  
    1.19  qed_goal "ch2ch_fappR" thy 
    1.20 - "is_chain(Y) ==> is_chain(%i. f`(Y i))"
    1.21 + "chain(Y) ==> chain(%i. f`(Y i))"
    1.22  (fn prems =>
    1.23          [
    1.24          (cut_facts_tac prems 1),
    1.25 @@ -147,7 +147,7 @@
    1.26  
    1.27  
    1.28  bind_thm ("ch2ch_fappL", monofun_fapp1 RS ch2ch_MF2L);
    1.29 -(* is_chain(?F) ==> is_chain (%i. ?F i`?x)                                  *)
    1.30 +(* chain(?F) ==> chain (%i. ?F i`?x)                                  *)
    1.31  
    1.32  
    1.33  (* ------------------------------------------------------------------------ *)
    1.34 @@ -156,7 +156,7 @@
    1.35  (* ------------------------------------------------------------------------ *)
    1.36  
    1.37  qed_goal "lub_cfun_mono" thy 
    1.38 -        "is_chain(F) ==> monofun(% x. lub(range(% j.(F j)`x)))"
    1.39 +        "chain(F) ==> monofun(% x. lub(range(% j.(F j)`x)))"
    1.40  (fn prems =>
    1.41          [
    1.42          (cut_facts_tac prems 1),
    1.43 @@ -172,7 +172,7 @@
    1.44  (* ------------------------------------------------------------------------ *)
    1.45  
    1.46  qed_goal "ex_lubcfun" thy
    1.47 -        "[| is_chain(F); is_chain(Y) |] ==>\
    1.48 +        "[| chain(F); chain(Y) |] ==>\
    1.49  \               lub(range(%j. lub(range(%i. F(j)`(Y i))))) =\
    1.50  \               lub(range(%i. lub(range(%j. F(j)`(Y i)))))"
    1.51  (fn prems =>
    1.52 @@ -190,7 +190,7 @@
    1.53  (* ------------------------------------------------------------------------ *)
    1.54  
    1.55  qed_goal "cont_lubcfun" thy 
    1.56 -        "is_chain(F) ==> cont(% x. lub(range(% j. F(j)`x)))"
    1.57 +        "chain(F) ==> cont(% x. lub(range(% j. F(j)`x)))"
    1.58  (fn prems =>
    1.59          [
    1.60          (cut_facts_tac prems 1),
    1.61 @@ -209,7 +209,7 @@
    1.62  (* ------------------------------------------------------------------------ *)
    1.63  
    1.64  qed_goal "lub_cfun" thy 
    1.65 -  "is_chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)`x)))"
    1.66 +  "chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)`x)))"
    1.67  (fn prems =>
    1.68          [
    1.69          (cut_facts_tac prems 1),
    1.70 @@ -233,11 +233,11 @@
    1.71  
    1.72  bind_thm ("thelub_cfun", lub_cfun RS thelubI);
    1.73  (* 
    1.74 -is_chain(?CCF1) ==>  lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x)))
    1.75 +chain(?CCF1) ==>  lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x)))
    1.76  *)
    1.77  
    1.78  qed_goal "cpo_cfun" thy 
    1.79 -  "is_chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x"
    1.80 +  "chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x"
    1.81  (fn prems =>
    1.82          [
    1.83          (cut_facts_tac prems 1),