# HG changeset patch
# User oheimb
# Date 889551193 -3600
# Node ID c8a8482a812488451fbd408958de203fd95ef22e
# Parent  c1b83b42f65ab5dc262c16c81ad92eb94f40eab7
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin

diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/Cfun2.ML
--- 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),
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/Cfun3.ML
--- a/src/HOLCF/Cfun3.ML	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Cfun3.ML	Tue Mar 10 18:33:13 1998 +0100
@@ -52,7 +52,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "contlub_cfun_fun" thy 
-"is_chain(FY) ==>\
+"chain(FY) ==>\
 \ lub(range FY)`x = lub(range (%i. FY(i)`x))"
 (fn prems =>
         [
@@ -66,7 +66,7 @@
 
 
 qed_goal "cont_cfun_fun" thy 
-"is_chain(FY) ==>\
+"chain(FY) ==>\
 \ range(%i. FY(i)`x) <<| lub(range FY)`x"
 (fn prems =>
         [
@@ -82,7 +82,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "contlub_cfun" thy 
-"[|is_chain(FY);is_chain(TY)|] ==>\
+"[|chain(FY);chain(TY)|] ==>\
 \ (lub(range FY))`(lub(range TY)) = lub(range(%i. FY(i)`(TY i)))"
 (fn prems =>
         [
@@ -96,7 +96,7 @@
         ]);
 
 qed_goal "cont_cfun" thy 
-"[|is_chain(FY);is_chain(TY)|] ==>\
+"[|chain(FY);chain(TY)|] ==>\
 \ range(%i.(FY i)`(TY i)) <<| (lub (range FY))`(lub(range TY))"
 (fn prems =>
         [
@@ -373,11 +373,11 @@
 (*simpset_ref() := simpset() addsolver (K (DEPTH_SOLVE_1 o cont_tac));*)
 
 (* ------------------------------------------------------------------------ *)
-(* some lemmata for functions with flat/chain_finite domain/range types	    *)
+(* some lemmata for functions with flat/chfin domain/range types	    *)
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "chfin_fappR" thy 
-    "is_chain (Y::nat => 'a::cpo->'b::chfin)==> !s. ? n. lub(range(Y))`s = Y n`s" 
+    "chain (Y::nat => 'a::cpo->'b::chfin)==> !s. ? n. lub(range(Y))`s = Y n`s" 
 (fn prems => 
 	[
 	cut_facts_tac prems 1,
@@ -441,15 +441,15 @@
 (* propagation of flatness and chainfiniteness by continuous isomorphisms   *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "chfin2chfin" thy "!!f g.[|! Y::nat=>'a. is_chain Y --> (? n. max_in_chain n Y); \
+qed_goal "chfin2chfin" thy "!!f g.[|! Y::nat=>'a. chain Y --> (? n. max_in_chain n Y); \
 \ !y. f`(g`y)=(y::'b) ; !x. g`(f`x)=(x::'a::chfin) |] \
-\ ==> ! Y::nat=>'b. is_chain Y --> (? n. max_in_chain n Y)"
+\ ==> ! Y::nat=>'b. chain Y --> (? n. max_in_chain n Y)"
  (fn prems =>
         [
         (rewtac max_in_chain_def),
         (strip_tac 1),
         (rtac exE 1),
-        (res_inst_tac [("P","is_chain(%i. g`(Y i))")] mp 1),
+        (res_inst_tac [("P","chain(%i. g`(Y i))")] mp 1),
         (etac spec 1),
         (etac ch2ch_fappR 1),
         (rtac exI 1),
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/Cont.ML
--- a/src/HOLCF/Cont.ML	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Cont.ML	Tue Mar 10 18:33:13 1998 +0100
@@ -13,7 +13,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goalw "contlubI" thy [contlub]
-        "! Y. is_chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))==>\
+        "! Y. chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))==>\
 \        contlub(f)"
 (fn prems =>
         [
@@ -23,7 +23,7 @@
 
 qed_goalw "contlubE" thy [contlub]
         " contlub(f)==>\
-\         ! Y. is_chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))"
+\         ! Y. chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -32,7 +32,7 @@
 
 
 qed_goalw "contI" thy [cont]
- "! Y. is_chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y))) ==> cont(f)"
+ "! Y. chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y))) ==> cont(f)"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -40,7 +40,7 @@
         ]);
 
 qed_goalw "contE" thy [cont]
- "cont(f) ==> ! Y. is_chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y)))"
+ "cont(f) ==> ! Y. chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y)))"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -74,14 +74,14 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "ch2ch_monofun" thy 
-        "[| monofun(f); is_chain(Y) |] ==> is_chain(%i. f(Y(i)))"
+        "[| monofun(f); chain(Y) |] ==> chain(%i. f(Y(i)))"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (rtac is_chainI 1),
+        (rtac chainI 1),
         (rtac allI 1),
         (etac (monofunE RS spec RS spec RS mp) 1),
-        (etac (is_chainE RS spec) 1)
+        (etac (chainE RS spec) 1)
         ]);
 
 (* ------------------------------------------------------------------------ *)
@@ -194,7 +194,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "ch2ch_MF2L" thy 
-"[|monofun(MF2); is_chain(F)|] ==> is_chain(%i. MF2 (F i) x)"
+"[|monofun(MF2); chain(F)|] ==> chain(%i. MF2 (F i) x)"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -204,7 +204,7 @@
 
 
 qed_goal "ch2ch_MF2R" thy 
-"[|monofun(MF2(f)); is_chain(Y)|] ==> is_chain(%i. MF2 f (Y i))"
+"[|monofun(MF2(f)); chain(Y)|] ==> chain(%i. MF2 f (Y i))"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -213,36 +213,36 @@
         ]);
 
 qed_goal "ch2ch_MF2LR" thy 
-"[|monofun(MF2); !f. monofun(MF2(f)); is_chain(F); is_chain(Y)|] ==> \
-\  is_chain(%i. MF2(F(i))(Y(i)))"
+"[|monofun(MF2); !f. monofun(MF2(f)); chain(F); chain(Y)|] ==> \
+\  chain(%i. MF2(F(i))(Y(i)))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (rtac is_chainI 1),
+        (rtac chainI 1),
         (strip_tac 1 ),
         (rtac trans_less 1),
-        (etac (ch2ch_MF2L RS is_chainE RS spec) 1),
+        (etac (ch2ch_MF2L RS chainE RS spec) 1),
         (atac 1),
         ((rtac (monofunE RS spec RS spec RS mp) 1) THEN (etac spec 1)),
-        (etac (is_chainE RS spec) 1)
+        (etac (chainE RS spec) 1)
         ]);
 
 
 qed_goal "ch2ch_lubMF2R" thy 
 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
 \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
-\       is_chain(F);is_chain(Y)|] ==> \
-\       is_chain(%j. lub(range(%i. MF2 (F j) (Y i))))"
+\       chain(F);chain(Y)|] ==> \
+\       chain(%j. lub(range(%i. MF2 (F j) (Y i))))"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (rtac (lub_mono RS allI RS is_chainI) 1),
+        (rtac (lub_mono RS allI RS chainI) 1),
         ((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
         (atac 1),
         ((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
         (atac 1),
         (strip_tac 1),
-        (rtac (is_chainE RS spec) 1),
+        (rtac (chainE RS spec) 1),
         (etac ch2ch_MF2L 1),
         (atac 1)
         ]);
@@ -251,18 +251,18 @@
 qed_goal "ch2ch_lubMF2L" thy 
 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
 \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
-\       is_chain(F);is_chain(Y)|] ==> \
-\       is_chain(%i. lub(range(%j. MF2 (F j) (Y i))))"
+\       chain(F);chain(Y)|] ==> \
+\       chain(%i. lub(range(%j. MF2 (F j) (Y i))))"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (rtac (lub_mono RS allI RS is_chainI) 1),
+        (rtac (lub_mono RS allI RS chainI) 1),
         (etac ch2ch_MF2L 1),
         (atac 1),
         (etac ch2ch_MF2L 1),
         (atac 1),
         (strip_tac 1),
-        (rtac (is_chainE RS spec) 1),
+        (rtac (chainE RS spec) 1),
         ((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
         (atac 1)
         ]);
@@ -271,7 +271,7 @@
 qed_goal "lub_MF2_mono" thy 
 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
 \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
-\       is_chain(F)|] ==> \
+\       chain(F)|] ==> \
 \       monofun(% x. lub(range(% j. MF2 (F j) (x))))"
 (fn prems =>
         [
@@ -291,7 +291,7 @@
 qed_goal "ex_lubMF2" thy 
 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
 \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
-\       is_chain(F); is_chain(Y)|] ==> \
+\       chain(F); chain(Y)|] ==> \
 \               lub(range(%j. lub(range(%i. MF2(F j) (Y i))))) =\
 \               lub(range(%i. lub(range(%j. MF2(F j) (Y i)))))"
  (fn prems =>
@@ -330,7 +330,7 @@
 qed_goal "diag_lubMF2_1" thy 
 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
 \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
-\  is_chain(FY);is_chain(TY)|] ==>\
+\  chain(FY);chain(TY)|] ==>\
 \ lub(range(%i. lub(range(%j. MF2(FY(j))(TY(i)))))) =\
 \ lub(range(%i. MF2(FY(i))(TY(i))))"
  (fn prems =>
@@ -374,7 +374,7 @@
 qed_goal "diag_lubMF2_2" thy 
 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
 \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
-\  is_chain(FY);is_chain(TY)|] ==>\
+\  chain(FY);chain(TY)|] ==>\
 \ lub(range(%j. lub(range(%i. MF2(FY(j))(TY(i)))))) =\
 \ lub(range(%i. MF2(FY(i))(TY(i))))"
  (fn prems =>
@@ -394,7 +394,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "contlub_CF2" thy 
-"[|cont(CF2);!f. cont(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
+"[|cont(CF2);!f. cont(CF2(f));chain(FY);chain(TY)|] ==>\
 \ CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i. CF2(FY(i))(TY(i))))"
  (fn prems =>
         [
@@ -524,7 +524,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "contlub_abstraction" thy
-"[|is_chain(Y::nat=>'a);!y. cont(%x.(c::'a::cpo=>'b::cpo=>'c::cpo) x y)|] ==>\
+"[|chain(Y::nat=>'a);!y. cont(%x.(c::'a::cpo=>'b::cpo=>'c::cpo) x y)|] ==>\
 \ (%y. lub(range(%i. c (Y i) y))) = (lub(range(%i.%y. c (Y i) y)))"
  (fn prems =>
         [
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Cont.thy	Tue Mar 10 18:33:13 1998 +0100
@@ -27,10 +27,10 @@
 
 monofun         "monofun(f) == ! x y. x << y --> f(x) << f(y)"
 
-contlub         "contlub(f) == ! Y. is_chain(Y) --> 
+contlub         "contlub(f) == ! Y. chain(Y) --> 
                                 f(lub(range(Y))) = lub(range(% i. f(Y(i))))"
 
-cont            "cont(f)   == ! Y. is_chain(Y) --> 
+cont            "cont(f)   == ! Y. chain(Y) --> 
                                 range(% i. f(Y(i))) <<| f(lub(range(Y)))"
 
 (* ------------------------------------------------------------------------ *)
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/Cprod2.ML
--- a/src/HOLCF/Cprod2.ML	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Cprod2.ML	Tue Mar 10 18:33:13 1998 +0100
@@ -116,7 +116,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "lub_cprod" thy 
-"is_chain S ==> range S<<|(lub(range(%i. fst(S i))),lub(range(%i. snd(S i))))"
+"chain S ==> range S<<|(lub(range(%i. fst(S i))),lub(range(%i. snd(S i))))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -141,13 +141,13 @@
 
 bind_thm ("thelub_cprod", lub_cprod RS thelubI);
 (*
-"is_chain ?S1 ==>
+"chain ?S1 ==>
  lub (range ?S1) =
  (lub (range (%i. fst (?S1 i))), lub (range (%i. snd (?S1 i))))" : thm
 
 *)
 
-qed_goal "cpo_cprod" thy "is_chain(S::nat=>'a::cpo*'b::cpo)==>? x. range S<<| x"
+qed_goal "cpo_cprod" thy "chain(S::nat=>'a::cpo*'b::cpo)==>? x. range S<<| x"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/Cprod3.ML
--- a/src/HOLCF/Cprod3.ML	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Cprod3.ML	Tue Mar 10 18:33:13 1998 +0100
@@ -20,7 +20,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "Cprod3_lemma1" Cprod3.thy 
-"is_chain(Y::(nat=>'a::cpo)) ==>\
+"chain(Y::(nat=>'a::cpo)) ==>\
 \ (lub(range(Y)),(x::'b::cpo)) =\
 \ (lub(range(%i. fst(Y i,x))),lub(range(%i. snd(Y i,x))))"
  (fn prems =>
@@ -57,7 +57,7 @@
         ]);
 
 qed_goal "Cprod3_lemma2" Cprod3.thy 
-"is_chain(Y::(nat=>'a::cpo)) ==>\
+"chain(Y::(nat=>'a::cpo)) ==>\
 \ ((x::'b::cpo),lub(range Y)) =\
 \ (lub(range(%i. fst(x,Y i))),lub(range(%i. snd(x, Y i))))"
  (fn prems =>
@@ -261,7 +261,7 @@
         ]);
 
 qed_goalw "lub_cprod2" Cprod3.thy [cfst_def,csnd_def,cpair_def]
-"[|is_chain(S)|] ==> range(S) <<| \
+"[|chain(S)|] ==> range(S) <<| \
 \ <(lub(range(%i. cfst`(S i)))) , lub(range(%i. csnd`(S i)))>"
  (fn prems =>
         [
@@ -277,7 +277,7 @@
 
 bind_thm ("thelub_cprod2", lub_cprod2 RS thelubI);
 (*
-is_chain ?S1 ==>
+chain ?S1 ==>
  lub (range ?S1) =
  <lub (range (%i. cfst`(?S1 i))), lub (range (%i. csnd`(?S1 i)))>" 
 *)
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/Discrete.ML
--- a/src/HOLCF/Discrete.ML	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Discrete.ML	Tue Mar 10 18:33:13 1998 +0100
@@ -10,7 +10,7 @@
 Addsimps [undiscr_Discr];
 
 goal thy
- "!!S::nat=>('a::term)discr. is_chain(S) ==> range(%i. f(S i)) = {f(S 0)}";
+ "!!S::nat=>('a::term)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}";
 by (fast_tac (claset() addDs [discr_chain0] addEs [arg_cong]) 1);
 qed "discr_chain_f_range0";
 
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/Discrete1.ML
--- a/src/HOLCF/Discrete1.ML	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Discrete1.ML	Tue Mar 10 18:33:13 1998 +0100
@@ -11,8 +11,8 @@
 qed "discr_less_eq";
 AddIffs [discr_less_eq];
 
-goalw thy [is_chain]
- "!!S::nat=>('a::term)discr. is_chain S ==> S i = S 0";
+goalw thy [chain]
+ "!!S::nat=>('a::term)discr. chain S ==> S i = S 0";
 by (nat_ind_tac "i" 1);
 by (rtac refl 1);
 by (etac subst 1);
@@ -21,12 +21,12 @@
 qed "discr_chain0";
 
 goal thy
- "!!S::nat=>('a::term)discr. is_chain(S) ==> range(S) = {S 0}";
+ "!!S::nat=>('a::term)discr. chain(S) ==> range(S) = {S 0}";
 by (fast_tac (claset() addEs [discr_chain0]) 1);
 qed "discr_chain_range0";
 Addsimps [discr_chain_range0];
 
 goalw thy [is_lub,is_ub]
- "!!S. is_chain S ==> ? x::('a::term)discr. range(S) <<| x";
+ "!!S. chain S ==> ? x::('a::term)discr. range(S) <<| x";
 by (Asm_simp_tac 1);
 qed "discr_cpo";
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Fix.thy	Tue Mar 10 18:33:13 1998 +0100
@@ -24,7 +24,7 @@
 Ifix_def      "Ifix F == lub(range(%i. iterate i F UU))"
 fix_def       "fix == (LAM f. Ifix f)"
 
-adm_def       "adm P == !Y. is_chain(Y) --> 
+adm_def       "adm P == !Y. chain(Y) --> 
                         (!i. P(Y i)) --> P(lub(range Y))"
 
 admw_def      "admw P == !F. (!n. P (iterate n F UU)) -->
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/Fun1.thy
--- a/src/HOLCF/Fun1.thy	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Fun1.thy	Tue Mar 10 18:33:13 1998 +0100
@@ -12,7 +12,7 @@
 
 Fun1 = Pcpo +
 
-instance flat<chfin (flat_imp_chain_finite)
+instance flat<chfin (flat_imp_chfin)
 
 (* to make << defineable: *)
 instance fun  :: (term,sq_ord)sq_ord
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/Fun2.ML
--- a/src/HOLCF/Fun2.ML	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Fun2.ML	Tue Mar 10 18:33:13 1998 +0100
@@ -52,11 +52,11 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "ch2ch_fun" thy 
-        "is_chain(S::nat=>('a=>'b::po)) ==> is_chain(% i. S(i)(x))"
+        "chain(S::nat=>('a=>'b::po)) ==> chain(% i. S(i)(x))"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (rewtac is_chain),
+        (rewtac chain),
         (rtac allI 1),
         (rtac spec 1),
         (rtac (less_fun RS subst) 1),
@@ -86,7 +86,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "lub_fun"  Fun2.thy
-        "is_chain(S::nat=>('a::term => 'b::cpo)) ==> \
+        "chain(S::nat=>('a::term => 'b::cpo)) ==> \
 \        range(S) <<| (% x. lub(range(% i. S(i)(x))))"
 (fn prems =>
         [
@@ -108,10 +108,10 @@
         ]);
 
 bind_thm ("thelub_fun", lub_fun RS thelubI);
-(* is_chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *)
+(* chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *)
 
 qed_goal "cpo_fun"  Fun2.thy
-        "is_chain(S::nat=>('a::term => 'b::cpo)) ==> ? x. range(S) <<| x"
+        "chain(S::nat=>('a::term => 'b::cpo)) ==> ? x. range(S) <<| x"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/IOA/meta_theory/Sequence.ML
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Tue Mar 10 18:33:13 1998 +0100
@@ -920,12 +920,12 @@
 by (res_inst_tac [("t","s2")] (seq.reach RS subst)  1);
 by (rtac (fix_def2 RS ssubst ) 1);
 by (stac contlub_cfun_fun 1);
-by (rtac is_chain_iterate 1);
+by (rtac chain_iterate 1);
 by (stac contlub_cfun_fun 1);
-by (rtac is_chain_iterate 1);
+by (rtac chain_iterate 1);
 by (rtac lub_mono 1);
-by (rtac (is_chain_iterate RS ch2ch_fappL) 1);
-by (rtac (is_chain_iterate RS ch2ch_fappL) 1);
+by (rtac (chain_iterate RS ch2ch_fappL) 1);
+by (rtac (chain_iterate RS ch2ch_fappL) 1);
 by (rtac allI 1);
 by (resolve_tac prems 1);
 qed"take_lemma_less1";
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/Lift2.ML
--- a/src/HOLCF/Lift2.ML	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Lift2.ML	Tue Mar 10 18:33:13 1998 +0100
@@ -56,7 +56,7 @@
 (* Tailoring chain_mono2 of Pcpo.ML to Undef *)
 
 goal Lift2.thy
-"!!Y. [|? j.~Y(j)=Undef;is_chain(Y::nat=>('a)lift)|] \
+"!!Y. [|? j.~Y(j)=Undef;chain(Y::nat=>('a)lift)|] \
 \ ==> ? j.!i. j<i-->~Y(i)=Undef";
 by Safe_tac;
 by (Step_tac 1);
@@ -68,10 +68,10 @@
 qed"chain_mono2_po";
 
 
-(* Tailoring flat_imp_chain_finite of Fix.ML to lift *)
+(* Tailoring flat_imp_chfin of Fix.ML to lift *)
 
 goal Lift2.thy
-        "(! Y. is_chain(Y::nat=>('a)lift)-->(? n. max_in_chain n Y))";
+        "(! Y. chain(Y::nat=>('a)lift)-->(? n. max_in_chain n Y))";
 by (rewtac max_in_chain_def);  
 by (strip_tac 1);
 by (res_inst_tac [("P","!i. Y(i)=Undef")] case_split_thm  1);
@@ -104,14 +104,14 @@
 by (rtac mp 1); 
 by (etac spec 1); 
 by (Asm_simp_tac 1);
-qed"flat_imp_chain_finite_poo";
+qed"flat_imp_chfin_poo";
 
 
 (* Main Lemma: cpo_lift *)
 
 goal Lift2.thy  
-  "!!Y. is_chain(Y::nat=>('a)lift) ==> ? x. range(Y) <<|x";
-by (cut_inst_tac [] flat_imp_chain_finite_poo 1);
+  "!!Y. chain(Y::nat=>('a)lift) ==> ? x. range(Y) <<|x";
+by (cut_inst_tac [] flat_imp_chfin_poo 1);
 by (Step_tac 1);
 by Safe_tac;
 by (Step_tac 1); 
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/Pcpo.ML
--- a/src/HOLCF/Pcpo.ML	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Pcpo.ML	Tue Mar 10 18:33:13 1998 +0100
@@ -25,7 +25,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "thelubE"  thy 
-        "[| is_chain(S);lub(range(S)) = (l::'a::cpo)|] ==> range(S) <<| l "
+        "[| chain(S);lub(range(S)) = (l::'a::cpo)|] ==> range(S) <<| l "
 (fn prems =>
         [
         (cut_facts_tac prems 1), 
@@ -40,12 +40,12 @@
 
 
 bind_thm ("is_ub_thelub", cpo RS lubI RS is_ub_lub);
-(* is_chain(?S1) ==> ?S1(?x) << lub(range(?S1))                             *)
+(* chain(?S1) ==> ?S1(?x) << lub(range(?S1))                             *)
 
 bind_thm ("is_lub_thelub", cpo RS lubI RS is_lub_lub);
-(* [| is_chain(?S5); range(?S5) <| ?x1 |] ==> lub(range(?S5)) << ?x1        *)
+(* [| chain(?S5); range(?S5) <| ?x1 |] ==> lub(range(?S5)) << ?x1        *)
 
-qed_goal "maxinch_is_thelub" thy "is_chain Y ==> \
+qed_goal "maxinch_is_thelub" thy "chain Y ==> \
 \       max_in_chain i Y = (lub(range(Y)) = ((Y i)::'a::cpo))" 
 (fn prems => 
         [
@@ -65,7 +65,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "lub_mono" thy 
-        "[|is_chain(C1::(nat=>'a::cpo));is_chain(C2); ! k. C1(k) << C2(k)|]\
+        "[|chain(C1::(nat=>'a::cpo));chain(C2); ! k. C1(k) << C2(k)|]\
 \           ==> lub(range(C1)) << lub(range(C2))"
 (fn prems =>
         [
@@ -83,7 +83,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "lub_equal" thy
-"[| is_chain(C1::(nat=>'a::cpo));is_chain(C2);!k. C1(k)=C2(k)|]\
+"[| chain(C1::(nat=>'a::cpo));chain(C2);!k. C1(k)=C2(k)|]\
 \       ==> lub(range(C1))=lub(range(C2))"
 (fn prems =>
         [
@@ -108,7 +108,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "lub_mono2" thy 
-"[|? j.!i. j<i --> X(i::nat)=Y(i);is_chain(X::nat=>'a::cpo);is_chain(Y)|]\
+"[|? j.!i. j<i --> X(i::nat)=Y(i);chain(X::nat=>'a::cpo);chain(Y)|]\
 \ ==> lub(range(X))<<lub(range(Y))"
  (fn prems =>
         [
@@ -137,7 +137,7 @@
         ]);
 
 qed_goal "lub_equal2" thy 
-"[|? j.!i. j<i --> X(i)=Y(i);is_chain(X::nat=>'a::cpo);is_chain(Y)|]\
+"[|? j.!i. j<i --> X(i)=Y(i);chain(X::nat=>'a::cpo);chain(Y)|]\
 \ ==> lub(range(X))=lub(range(Y))"
  (fn prems =>
         [
@@ -153,7 +153,7 @@
         (Fast_tac 1)
         ]);
 
-qed_goal "lub_mono3" thy "[|is_chain(Y::nat=>'a::cpo);is_chain(X);\
+qed_goal "lub_mono3" thy "[|chain(Y::nat=>'a::cpo);chain(X);\
 \! i. ? j. Y(i)<< X(j)|]==> lub(range(Y))<<lub(range(X))"
  (fn prems =>
         [
@@ -206,7 +206,7 @@
         ]);
 
 qed_goal "chain_UU_I" thy
-        "[|is_chain(Y);lub(range(Y))=UU|] ==> ! i. Y(i)=UU"
+        "[|chain(Y);lub(range(Y))=UU|] ==> ! i. Y(i)=UU"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -256,7 +256,7 @@
 
 
 qed_goal "chain_mono2" thy 
-"[|? j.~Y(j)=UU;is_chain(Y::nat=>'a::pcpo)|]\
+"[|? j.~Y(j)=UU;chain(Y::nat=>'a::pcpo)|]\
 \ ==> ? j.!i. j<i-->~Y(i)=UU"
  (fn prems =>
         [
@@ -275,11 +275,11 @@
 (**************************************)
 
 (* ------------------------------------------------------------------------ *)
-(* flat types are chain_finite                                              *)
+(* flat types are chfin                                              *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "flat_imp_chain_finite" thy [max_in_chain_def]
-        "!Y::nat=>'a::flat. is_chain Y-->(? n. max_in_chain n Y)"
+qed_goalw "flat_imp_chfin" thy [max_in_chain_def]
+        "!Y::nat=>'a::flat. chain Y-->(? n. max_in_chain n Y)"
  (fn _ =>
         [
         (strip_tac 1),
@@ -309,7 +309,7 @@
 	]);
 
 qed_goal "chfin2finch" thy 
-    "is_chain (Y::nat=>'a::chfin) ==> finite_chain Y"
+    "chain (Y::nat=>'a::chfin) ==> finite_chain Y"
 	(fn prems => 
 	[
 	cut_facts_tac prems 1,
@@ -322,8 +322,8 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "infinite_chain_adm_lemma" Porder.thy 
-"[|is_chain Y; !i. P (Y i); \
-\  (!!Y. [| is_chain Y; !i. P (Y i); ~ finite_chain Y |] ==> P (lub (range Y)))\
+"[|chain Y; !i. P (Y i); \
+\  (!!Y. [| chain Y; !i. P (Y i); ~ finite_chain Y |] ==> P (lub (range Y)))\
 \ |] ==> P (lub (range Y))"
  (fn prems => [
         cut_facts_tac prems 1,
@@ -334,8 +334,8 @@
         etac (lub_finch1 RS thelubI RS ssubst) 1, atac 1, etac spec 1]);
 
 qed_goal "increasing_chain_adm_lemma" Porder.thy 
-"[|is_chain Y; !i. P (Y i); \
-\  (!!Y. [| is_chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j|]\
+"[|chain Y; !i. P (Y i); \
+\  (!!Y. [| chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j|]\
 \ ==> P (lub (range Y))) |] ==> P (lub (range Y))"
  (fn prems => [
         cut_facts_tac prems 1,
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Pcpo.thy	Tue Mar 10 18:33:13 1998 +0100
@@ -11,7 +11,7 @@
 (* ********************************************** *)
 axclass cpo < po
         (* class axiom: *)
-  cpo   "is_chain S ==> ? x. range(S) <<| (x::'a::po)" 
+  cpo   "chain S ==> ? x. range(S) <<| (x::'a::po)" 
 
 (* The class pcpo of pointed cpos *)
 (* ****************************** *)
@@ -32,7 +32,7 @@
 
 axclass chfin<cpo
 
-chfin 	"!Y. is_chain Y-->(? n. max_in_chain n Y)"
+chfin 	"!Y. chain Y-->(? n. max_in_chain n Y)"
 
 axclass flat<pcpo
 
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/Porder.ML
--- a/src/HOLCF/Porder.ML	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Porder.ML	Tue Mar 10 18:33:13 1998 +0100
@@ -28,7 +28,7 @@
 (* chains are monotone functions                                            *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "chain_mono" thy [is_chain] "is_chain F ==> x<y --> F x<<F y"
+qed_goalw "chain_mono" thy [chain] "chain F ==> x<y --> F x<<F y"
 ( fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -47,7 +47,7 @@
         (atac 1)
         ]);
 
-qed_goal "chain_mono3" thy "[| is_chain F; x <= y |] ==> F x << F y"
+qed_goal "chain_mono3" thy "[| chain F; x <= y |] ==> F x << F y"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -64,8 +64,8 @@
 (* The range of a chain is a totaly ordered     <<                           *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "chain_is_tord" thy [is_tord] 
-"!!F. is_chain(F) ==> is_tord(range(F))"
+qed_goalw "chain_tord" thy [tord] 
+"!!F. chain(F) ==> tord(range(F))"
  (fn _ =>
         [
         Safe_tac,
@@ -138,13 +138,13 @@
         (atac 1)
         ]);
 
-qed_goalw "is_chainE" thy [is_chain] "is_chain F ==> !i. F(i) << F(Suc(i))"
+qed_goalw "chainE" thy [chain] "chain F ==> !i. F(i) << F(Suc(i))"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
         (atac 1)]);
 
-qed_goalw "is_chainI" thy [is_chain] "!i. F i << F(Suc i) ==> is_chain F"
+qed_goalw "chainI" thy [chain] "!i. F i << F(Suc i) ==> chain F"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -185,7 +185,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goalw "lub_finch1" thy [max_in_chain_def]
-        "[| is_chain C; max_in_chain i C|] ==> range C <<| C i"
+        "[| chain C; max_in_chain i C|] ==> range C <<| C i"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -218,11 +218,11 @@
         ]);
 
 
-qed_goal "bin_chain" thy "x<<y ==> is_chain (%i. if i=0 then x else y)"
+qed_goal "bin_chain" thy "x<<y ==> chain (%i. if i=0 then x else y)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (rtac is_chainI 1),
+        (rtac chainI 1),
         (rtac allI 1),
         (nat_ind_tac "i" 1),
         (Asm_simp_tac 1),
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Porder.thy	Tue Mar 10 18:33:13 1998 +0100
@@ -13,8 +13,8 @@
         "<|"    ::      "['a set,'a::po] => bool"       (infixl 55)
         "<<|"   ::      "['a set,'a::po] => bool"       (infixl 55)
         lub     ::      "'a set => 'a::po"
-        is_tord ::      "'a::po set => bool"
-        is_chain ::     "(nat=>'a::po) => bool"
+        tord ::      "'a::po set => bool"
+        chain ::     "(nat=>'a::po) => bool"
         max_in_chain :: "[nat,nat=>'a::po]=>bool"
         finite_chain :: "(nat=>'a::po)=>bool"
 
@@ -37,14 +37,14 @@
 is_lub          "S <<| x == S <| x & (! u. S <| u  --> x << u)"
 
 (* Arbitrary chains are total orders    *)                  
-is_tord         "is_tord S == ! x y. x:S & y:S --> (x<<y | y<<x)"
+tord         "tord S == ! x y. x:S & y:S --> (x<<y | y<<x)"
 
 (* Here we use countable chains and I prefer to code them as functions! *)
-is_chain        "is_chain F == (! i. F(i) << F(Suc(i)))"
+chain        "chain F == (! i. F(i) << F(Suc(i)))"
 
 (* finite chains, needed for monotony of continouous functions *)
 max_in_chain_def "max_in_chain i C == ! j. i <= j --> C(i) = C(j)" 
-finite_chain_def "finite_chain C == is_chain(C) & (? i. max_in_chain i C)"
+finite_chain_def "finite_chain C == chain(C) & (? i. max_in_chain i C)"
 
 lub_def          "lub S == (@x. S <<| x)"
 
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/Sprod2.ML
--- a/src/HOLCF/Sprod2.ML	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Sprod2.ML	Tue Mar 10 18:33:13 1998 +0100
@@ -95,7 +95,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "lub_sprod" Sprod2.thy 
-"[|is_chain(S)|] ==> range(S) <<| \
+"[|chain(S)|] ==> range(S) <<| \
 \ Ispair (lub(range(%i. Isfst(S i)))) (lub(range(%i. Issnd(S i))))"
 (fn prems =>
         [
@@ -123,7 +123,7 @@
 
 
 qed_goal "cpo_sprod" Sprod2.thy 
-        "is_chain(S::nat=>'a**'b)==>? x. range(S)<<| x"
+        "chain(S::nat=>'a**'b)==>? x. range(S)<<| x"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/Sprod3.ML
--- a/src/HOLCF/Sprod3.ML	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Sprod3.ML	Tue Mar 10 18:33:13 1998 +0100
@@ -19,7 +19,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "sprod3_lemma1" thy 
-"[| is_chain(Y);  x~= UU;  lub(range(Y))~= UU |] ==>\
+"[| chain(Y);  x~= UU;  lub(range(Y))~= UU |] ==>\
 \ Ispair (lub(range Y)) x =\
 \ Ispair (lub(range(%i. Isfst(Ispair(Y i) x)))) \
 \        (lub(range(%i. Issnd(Ispair(Y i) x))))"
@@ -56,7 +56,7 @@
         ]);
 
 qed_goal "sprod3_lemma2" thy 
-"[| is_chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
+"[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
 \   Ispair (lub(range Y)) x =\
 \   Ispair (lub(range(%i. Isfst(Ispair(Y i) x))))\
 \          (lub(range(%i. Issnd(Ispair(Y i) x))))"
@@ -78,7 +78,7 @@
 
 
 qed_goal "sprod3_lemma3" thy 
-"[| is_chain(Y); x = UU |] ==>\
+"[| chain(Y); x = UU |] ==>\
 \          Ispair (lub(range Y)) x =\
 \          Ispair (lub(range(%i. Isfst(Ispair (Y i) x))))\
 \                 (lub(range(%i. Issnd(Ispair (Y i) x))))"
@@ -124,7 +124,7 @@
         ]);
 
 qed_goal "sprod3_lemma4" thy 
-"[| is_chain(Y); x ~= UU; lub(range(Y)) ~= UU |] ==>\
+"[| chain(Y); x ~= UU; lub(range(Y)) ~= UU |] ==>\
 \         Ispair x (lub(range Y)) =\
 \         Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))\
 \                (lub(range(%i. Issnd (Ispair x (Y i)))))"
@@ -160,7 +160,7 @@
         ]);
 
 qed_goal "sprod3_lemma5" thy 
-"[| is_chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
+"[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
 \         Ispair x (lub(range Y)) =\
 \         Ispair (lub(range(%i. Isfst(Ispair x (Y i)))))\
 \                (lub(range(%i. Issnd(Ispair x (Y i)))))"
@@ -181,7 +181,7 @@
         ]);
 
 qed_goal "sprod3_lemma6" thy 
-"[| is_chain(Y); x = UU |] ==>\
+"[| chain(Y); x = UU |] ==>\
 \         Ispair x (lub(range Y)) =\
 \         Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))\
 \                (lub(range(%i. Issnd (Ispair x (Y i)))))"
@@ -563,7 +563,7 @@
 
 
 qed_goalw "lub_sprod2" thy [sfst_def,ssnd_def,spair_def]
-"[|is_chain(S)|] ==> range(S) <<| \
+"[|chain(S)|] ==> range(S) <<| \
 \ (| lub(range(%i. sfst`(S i))), lub(range(%i. ssnd`(S i))) |)"
  (fn prems =>
         [
@@ -580,7 +580,7 @@
 
 bind_thm ("thelub_sprod2", lub_sprod2 RS thelubI);
 (*
- "is_chain ?S1 ==>
+ "chain ?S1 ==>
  lub (range ?S1) =
  (|lub (range (%i. sfst`(?S1 i))), lub (range (%i. ssnd`(?S1 i)))|)" : thm
 *)
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/Ssum2.ML
--- a/src/HOLCF/Ssum2.ML	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Ssum2.ML	Tue Mar 10 18:33:13 1998 +0100
@@ -198,7 +198,7 @@
 
 
 qed_goal "ssum_lemma3" thy 
-"[|is_chain(Y);(? i x. Y(i)=Isinr(x::'b) & (x::'b)~=UU)|] ==>\
+"[|chain(Y);(? i x. Y(i)=Isinr(x::'b) & (x::'b)~=UU)|] ==>\
 \ (!i.? y. Y(i)=Isinr(y))"
  (fn prems =>
         [
@@ -231,7 +231,7 @@
         ]);
 
 qed_goal "ssum_lemma4" thy 
-"is_chain(Y) ==> (!i.? x. Y(i)=Isinl(x))|(!i.? y. Y(i)=Isinr(y))"
+"chain(Y) ==> (!i.? x. Y(i)=Isinl(x))|(!i.? y. Y(i)=Isinr(y))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -317,7 +317,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "lub_ssum1a" thy 
-"[|is_chain(Y);(!i.? x. Y(i)=Isinl(x))|] ==>\
+"[|chain(Y);(!i.? x. Y(i)=Isinl(x))|] ==>\
 \ range(Y) <<|\
 \ Isinl(lub(range(%i.(Iwhen (LAM x. x) (LAM y. UU))(Y i))))"
  (fn prems =>
@@ -358,7 +358,7 @@
 
 
 qed_goal "lub_ssum1b" thy 
-"[|is_chain(Y);(!i.? x. Y(i)=Isinr(x))|] ==>\
+"[|chain(Y);(!i.? x. Y(i)=Isinr(x))|] ==>\
 \ range(Y) <<|\
 \ Isinr(lub(range(%i.(Iwhen (LAM y. UU) (LAM x. x))(Y i))))"
  (fn prems =>
@@ -400,20 +400,20 @@
 
 bind_thm ("thelub_ssum1a", lub_ssum1a RS thelubI);
 (*
-[| is_chain ?Y1; ! i. ? x. ?Y1 i = Isinl x |] ==>
+[| chain ?Y1; ! i. ? x. ?Y1 i = Isinl x |] ==>
  lub (range ?Y1) = Isinl
  (lub (range (%i. Iwhen (LAM x. x) (LAM y. UU) (?Y1 i))))
 *)
 
 bind_thm ("thelub_ssum1b", lub_ssum1b RS thelubI);
 (*
-[| is_chain ?Y1; ! i. ? x. ?Y1 i = Isinr x |] ==>
+[| chain ?Y1; ! i. ? x. ?Y1 i = Isinr x |] ==>
  lub (range ?Y1) = Isinr
  (lub (range (%i. Iwhen (LAM y. UU) (LAM x. x) (?Y1 i))))
 *)
 
 qed_goal "cpo_ssum" thy 
-        "is_chain(Y::nat=>'a ++'b) ==> ? x. range(Y) <<|x"
+        "chain(Y::nat=>'a ++'b) ==> ? x. range(Y) <<|x"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/Ssum3.ML
--- a/src/HOLCF/Ssum3.ML	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Ssum3.ML	Tue Mar 10 18:33:13 1998 +0100
@@ -156,7 +156,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "ssum_lemma9" Ssum3.thy 
-"[| is_chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x. Y(i)=Isinl(x)"
+"[| chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x. Y(i)=Isinl(x)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -174,7 +174,7 @@
 
 
 qed_goal "ssum_lemma10" Ssum3.thy 
-"[| is_chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x. Y(i)=Isinr(x)"
+"[| chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x. Y(i)=Isinr(x)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -193,7 +193,7 @@
         ]);
 
 qed_goal "ssum_lemma11" Ssum3.thy 
-"[| is_chain(Y); lub(range(Y)) = Isinl(UU) |] ==>\
+"[| chain(Y); lub(range(Y)) = Isinl(UU) |] ==>\
 \   Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
  (fn prems =>
         [
@@ -210,7 +210,7 @@
         ]);
 
 qed_goal "ssum_lemma12" Ssum3.thy 
-"[| is_chain(Y); lub(range(Y)) = Isinl(x); x ~= UU |] ==>\
+"[| chain(Y); lub(range(Y)) = Isinl(x); x ~= UU |] ==>\
 \   Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
  (fn prems =>
         [
@@ -269,7 +269,7 @@
 
 
 qed_goal "ssum_lemma13" Ssum3.thy 
-"[| is_chain(Y); lub(range(Y)) = Isinr(x); x ~= UU |] ==>\
+"[| chain(Y); lub(range(Y)) = Isinr(x); x ~= UU |] ==>\
 \   Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
  (fn prems =>
         [
@@ -579,7 +579,7 @@
         ]);
 
 qed_goalw "ssum_chainE" Ssum3.thy [sinl_def,sinr_def] 
-        "is_chain(Y) ==> (!i.? x.(Y i)=sinl`x)|(!i.? y.(Y i)=sinr`y)"
+        "chain(Y) ==> (!i.? x.(Y i)=sinl`x)|(!i.? y.(Y i)=sinr`y)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -589,7 +589,7 @@
 
 
 qed_goalw "thelub_ssum2a" Ssum3.thy [sinl_def,sinr_def,sswhen_def] 
-"[| is_chain(Y); !i.? x. Y(i) = sinl`x |] ==>\ 
+"[| chain(Y); !i.? x. Y(i) = sinl`x |] ==>\ 
 \   lub(range(Y)) = sinl`(lub(range(%i. sswhen`(LAM x. x)`(LAM y. UU)`(Y i))))"
  (fn prems =>
         [
@@ -614,7 +614,7 @@
         ]);
 
 qed_goalw "thelub_ssum2b" Ssum3.thy [sinl_def,sinr_def,sswhen_def] 
-"[| is_chain(Y); !i.? x. Y(i) = sinr`x |] ==>\ 
+"[| chain(Y); !i.? x. Y(i) = sinr`x |] ==>\ 
 \   lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x. x)`(Y i))))"
  (fn prems =>
         [
@@ -641,7 +641,7 @@
         ]);
 
 qed_goalw "thelub_ssum2a_rev" Ssum3.thy [sinl_def,sinr_def] 
-        "[| is_chain(Y); lub(range(Y)) = sinl`x|] ==> !i.? x. Y(i)=sinl`x"
+        "[| chain(Y); lub(range(Y)) = sinl`x|] ==> !i.? x. Y(i)=sinl`x"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -655,7 +655,7 @@
         ]);
 
 qed_goalw "thelub_ssum2b_rev" Ssum3.thy [sinl_def,sinr_def] 
-        "[| is_chain(Y); lub(range(Y)) = sinr`x|] ==> !i.? x. Y(i)=sinr`x"
+        "[| chain(Y); lub(range(Y)) = sinr`x|] ==> !i.? x. Y(i)=sinr`x"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -669,7 +669,7 @@
         ]);
 
 qed_goal "thelub_ssum3" Ssum3.thy  
-"is_chain(Y) ==>\ 
+"chain(Y) ==>\ 
 \   lub(range(Y)) = sinl`(lub(range(%i. sswhen`(LAM x. x)`(LAM y. UU)`(Y i))))\
 \ | lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x. x)`(Y i))))"
  (fn prems =>
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/Up2.ML
--- a/src/HOLCF/Up2.ML	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Up2.ML	Tue Mar 10 18:33:13 1998 +0100
@@ -111,7 +111,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "lub_up1a" thy 
-"[|is_chain(Y);? i x. Y(i)=Iup(x)|] ==>\
+"[|chain(Y);? i x. Y(i)=Iup(x)|] ==>\
 \ range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x. x) (Y(i))))))"
  (fn prems =>
         [
@@ -148,7 +148,7 @@
         ]);
 
 qed_goal "lub_up1b" thy 
-"[|is_chain(Y);!i x. Y(i)~=Iup(x)|] ==>\
+"[|chain(Y);!i x. Y(i)~=Iup(x)|] ==>\
 \ range(Y) <<| Abs_Up (Inl ())"
  (fn prems =>
         [
@@ -172,18 +172,18 @@
 
 bind_thm ("thelub_up1a", lub_up1a RS thelubI);
 (*
-[| is_chain ?Y1; ? i x. ?Y1 i = Iup x |] ==>
+[| chain ?Y1; ? i x. ?Y1 i = Iup x |] ==>
  lub (range ?Y1) = Iup (lub (range (%i. Iup (LAM x. x) (?Y1 i))))
 *)
 
 bind_thm ("thelub_up1b", lub_up1b RS thelubI);
 (*
-[| is_chain ?Y1; ! i x. ?Y1 i ~= Iup x |] ==>
+[| chain ?Y1; ! i x. ?Y1 i ~= Iup x |] ==>
  lub (range ?Y1) = UU_up
 *)
 
 qed_goal "cpo_up" thy 
-        "is_chain(Y::nat=>('a)u) ==> ? x. range(Y) <<|x"
+        "chain(Y::nat=>('a)u) ==> ? x. range(Y) <<|x"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/Up3.ML
--- a/src/HOLCF/Up3.ML	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Up3.ML	Tue Mar 10 18:33:13 1998 +0100
@@ -230,7 +230,7 @@
         ]);
 
 qed_goalw "thelub_up2a" thy [up_def,fup_def] 
-"[| is_chain(Y); ? i x. Y(i) = up`x |] ==>\
+"[| chain(Y); ? i x. Y(i) = up`x |] ==>\
 \      lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))"
  (fn prems =>
         [
@@ -255,7 +255,7 @@
 
 
 qed_goalw "thelub_up2b" thy [up_def,fup_def] 
-"[| is_chain(Y); ! i x. Y(i) ~= up`x |] ==> lub(range(Y)) = UU"
+"[| chain(Y); ! i x. Y(i) ~= up`x |] ==> lub(range(Y)) = UU"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -289,7 +289,7 @@
 
 
 qed_goal "thelub_up2a_rev" thy  
-"[| is_chain(Y); lub(range(Y)) = up`x |] ==> ? i x. Y(i) = up`x"
+"[| chain(Y); lub(range(Y)) = up`x |] ==> ? i x. Y(i) = up`x"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -303,7 +303,7 @@
         ]);
 
 qed_goal "thelub_up2b_rev" thy  
-"[| is_chain(Y); lub(range(Y)) = UU |] ==> ! i x.  Y(i) ~= up`x"
+"[| chain(Y); lub(range(Y)) = UU |] ==> ! i x.  Y(i) ~= up`x"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -316,7 +316,7 @@
 
 
 qed_goal "thelub_up3" thy  
-"is_chain(Y) ==> lub(range(Y)) = UU |\
+"chain(Y) ==> lub(range(Y)) = UU |\
 \                lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))"
  (fn prems =>
         [
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/adm.ML
--- a/src/HOLCF/adm.ML	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/adm.ML	Tue Mar 10 18:33:13 1998 +0100
@@ -10,7 +10,7 @@
   [| cont t; adm P |] ==> adm (%x. P (t x))
 
 "t" is instantiated with a term of chain-finite type, so that
-adm_chain_finite can be applied:
+adm_chfin can be applied:
 
   adm (P::'a::{chfin,pcpo} => bool)
 
@@ -177,7 +177,7 @@
                 compose_tac (false, rule, 2) i THEN
                 rtac cont_thm i THEN
                 REPEAT (assume_tac i) THEN
-                rtac adm_chain_finite i
+                rtac adm_chfin i
               end 
           | [] => no_tac)
         end)
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/domain/theorems.ML	Tue Mar 10 18:33:13 1998 +0100
@@ -41,7 +41,7 @@
                                 asm_simp_tac (HOLCF_ss addsimps rews) i;
 
 val chain_tac = REPEAT_DETERM o resolve_tac 
-                [is_chain_iterate, ch2ch_fappR, ch2ch_fappL];
+                [chain_iterate, ch2ch_fappR, ch2ch_fappL];
 
 (* ----- general proofs ----------------------------------------------------- *)
 
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/ex/Stream.ML
--- a/src/HOLCF/ex/Stream.ML	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/ex/Stream.ML	Tue Mar 10 18:33:13 1998 +0100
@@ -136,12 +136,12 @@
 	(stac fix_def2 1),
 	(rewrite_goals_tac [stream.take_def]),
 	(stac contlub_cfun_fun 1),
-	(rtac is_chain_iterate 1),
+	(rtac chain_iterate 1),
 	(rtac refl 1)
 	]);
 
-qed_goal "chain_stream_take" thy "is_chain (%i. stream_take i`s)" (fn _ => [
-	rtac is_chainI 1,
+qed_goal "chain_stream_take" thy "chain (%i. stream_take i`s)" (fn _ => [
+	rtac chainI 1,
 	subgoal_tac "!i s. stream_take i`s << stream_take (Suc i)`s" 1,
 	fast_tac HOL_cs 1,
 	rtac allI 1,
@@ -160,10 +160,10 @@
 		rtac monofun_cfun_fun 1,
 		stac fix_def2 1,
 		rtac is_ub_thelub 1,
-		rtac is_chain_iterate 1,
+		rtac chain_iterate 1,
 		etac subst 1, (* 2*back(); *)
 		rtac monofun_cfun_fun 1,
-		rtac (rewrite_rule [is_chain] is_chain_iterate RS spec) 1]);
+		rtac (rewrite_rule [chain] chain_iterate RS spec) 1]);
 
 (*
 val stream_take_lemma2 = prove_goal thy 
diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/ex/loeckx.ML
--- a/src/HOLCF/ex/loeckx.ML	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/ex/loeckx.ML	Tue Mar 10 18:33:13 1998 +0100
@@ -8,13 +8,13 @@
 by (rtac ch2ch_fun 1);
 back();
 by (rtac refl 2);
-by (rtac is_chainI 1);
+by (rtac chainI 1);
 by (strip_tac 1);
 by (rtac (less_fun RS iffD2) 1);
 by (strip_tac 1);
 by (rtac (less_fun RS iffD2) 1);
 by (strip_tac 1);
-by (rtac (is_chain_iterate RS is_chainE RS spec) 1);
+by (rtac (chain_iterate RS chainE RS spec) 1);
 val loeckx_sieber = result();
 
 (* 
@@ -27,7 +27,7 @@
 Since we already proved the theorem
 
 val cont_lubcfun = prove_goal Cfun2.thy 
-        "is_chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))"
+        "chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))"
 
 
 it suffices to prove:
@@ -64,7 +64,7 @@
 by (rtac cont_iterate 1);
 by (rtac refl 1);
 by (rtac cont_lubcfun 1);
-by (rtac is_chainI 1);
+by (rtac chainI 1);
 by (strip_tac 1);
 by (rtac less_cfun2 1);
 by (stac beta_cfun 1);
@@ -73,7 +73,7 @@
 by (stac beta_cfun 1);
 by (rtac  cont2cont_CF1L 1);
 by (rtac cont_iterate 1);
-by (rtac (is_chain_iterate RS is_chainE RS spec) 1);
+by (rtac (chain_iterate RS chainE RS spec) 1);
 val cont_Ifix2 = result();
 
 (* the proof in little steps *)
@@ -97,14 +97,14 @@
 
 (*
 - cont_lubcfun;
-val it = "is_chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))" : thm   
+val it = "chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))" : thm   
 
 *)
 
 val prems = goal Fix.thy "cont Ifix";
 by (stac fix_lemma2 1);
 by (rtac cont_lubcfun 1);
-by (rtac is_chainI 1);
+by (rtac chainI 1);
 by (strip_tac 1);
 by (rtac less_cfun2 1);
 by (stac beta_cfun 1);
@@ -113,6 +113,6 @@
 by (stac beta_cfun 1);
 by (rtac  cont2cont_CF1L 1);
 by (rtac cont_iterate 1);
-by (rtac (is_chain_iterate RS is_chainE RS spec) 1);
+by (rtac (chain_iterate RS chainE RS spec) 1);
 val cont_Ifix2 = result();