src/HOLCF/Up3.ML

         (simp_tac (Up0_ss addsimps [cont_Iup]) 1),
         (rtac less_up2c 1)
         ]);
 
 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 =>
         [
         (cut_facts_tac prems 1),
         (stac beta_cfun 1),

         ]);
 
 
 
 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),
         (stac inst_up_pcpo 1),
         (rtac thelub_up1b 1),

         (etac exI 1)
         ]);
 
 
 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),
         (rtac exE 1),
         (rtac chain_UU_I_inverse2 1),

         (rtac (up_lemma2 RS iffD2) 1),
         (atac 1)
         ]);
 
 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),
         (rtac allI 1),
         (rtac (not_ex RS iffD1) 1),

         (fast_tac (HOL_cs addSDs [chain_UU_I RS spec]) 1)
         ]);
 
 
 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 =>
         [
         (cut_facts_tac prems 1),
         (rtac disjE 1),