--- a/src/HOLCF/Cfun2.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Cfun2.ML Tue Mar 10 18:33:13 1998 +0100
@@ -75,10 +75,10 @@
(* ------------------------------------------------------------------------ *)
bind_thm ("cont_cfun_arg", (cont_fapp2 RS contE RS spec RS mp));
-(* is_chain(?x1) ==> range (%i. ?fo3`(?x1 i)) <<| ?fo3`(lub (range ?x1)) *)
+(* chain(?x1) ==> range (%i. ?fo3`(?x1 i)) <<| ?fo3`(lub (range ?x1)) *)
bind_thm ("contlub_cfun_arg", (contlub_fapp2 RS contlubE RS spec RS mp));
-(* is_chain(?x1) ==> ?fo4`(lub (range ?x1)) = lub (range (%i. ?fo4`(?x1 i))) *)
+(* chain(?x1) ==> ?fo4`(lub (range ?x1)) = lub (range (%i. ?fo4`(?x1 i))) *)
(* ------------------------------------------------------------------------ *)
@@ -138,7 +138,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "ch2ch_fappR" thy
- "is_chain(Y) ==> is_chain(%i. f`(Y i))"
+ "chain(Y) ==> chain(%i. f`(Y i))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -147,7 +147,7 @@
bind_thm ("ch2ch_fappL", monofun_fapp1 RS ch2ch_MF2L);
-(* is_chain(?F) ==> is_chain (%i. ?F i`?x) *)
+(* chain(?F) ==> chain (%i. ?F i`?x) *)
(* ------------------------------------------------------------------------ *)
@@ -156,7 +156,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "lub_cfun_mono" thy
- "is_chain(F) ==> monofun(% x. lub(range(% j.(F j)`x)))"
+ "chain(F) ==> monofun(% x. lub(range(% j.(F j)`x)))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -172,7 +172,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "ex_lubcfun" thy
- "[| is_chain(F); is_chain(Y) |] ==>\
+ "[| chain(F); chain(Y) |] ==>\
\ lub(range(%j. lub(range(%i. F(j)`(Y i))))) =\
\ lub(range(%i. lub(range(%j. F(j)`(Y i)))))"
(fn prems =>
@@ -190,7 +190,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "cont_lubcfun" thy
- "is_chain(F) ==> cont(% x. lub(range(% j. F(j)`x)))"
+ "chain(F) ==> cont(% x. lub(range(% j. F(j)`x)))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -209,7 +209,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "lub_cfun" thy
- "is_chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)`x)))"
+ "chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)`x)))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -233,11 +233,11 @@
bind_thm ("thelub_cfun", lub_cfun RS thelubI);
(*
-is_chain(?CCF1) ==> lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x)))
+chain(?CCF1) ==> lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x)))
*)
qed_goal "cpo_cfun" thy
- "is_chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x"
+ "chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x"
(fn prems =>
[
(cut_facts_tac prems 1),