src/HOLCF/Completion.thy

   shows "chain (\<lambda>i. lub (f ` take i ` rep x))"
  apply (rule chainI)
  apply (rule is_lub_thelub0)
   apply (rule basis_fun_lemma0, erule f_mono)
  apply (rule is_ubI, clarsimp, rename_tac a)
- apply (rule sq_le.trans_less [OF f_mono [OF take_chain]])
+ apply (rule trans_less [OF f_mono [OF take_chain]])
  apply (rule is_ub_thelub0)
   apply (rule basis_fun_lemma0, erule f_mono)
  apply simp
 done
 

  apply (rule is_lub_thelub [OF _ ub_rangeI])
   apply (rule basis_fun_lemma1, erule f_mono)
  apply (rule is_lub_thelub0)
   apply (rule basis_fun_lemma0, erule f_mono)
  apply (rule is_ubI, clarsimp, rename_tac a)
- apply (rule sq_le.trans_less [OF f_mono [OF take_less]])
+ apply (rule trans_less [OF f_mono [OF take_less]])
  apply (erule (1) ub_imageD)
 done
 
 lemma basis_fun_lemma:
   fixes f :: "'a::type \<Rightarrow> 'c::cpo"

  apply (rule less_cfun_ext)
  apply (simp only: basis_fun_beta f_mono g_mono)
  apply (rule is_lub_thelub0)
   apply (rule basis_fun_lemma, erule f_mono)
  apply (rule ub_imageI, rename_tac a)
- apply (rule sq_le.trans_less [OF less])
+ apply (rule trans_less [OF less])
  apply (rule is_ub_thelub0)
   apply (rule basis_fun_lemma, erule g_mono)
  apply (erule imageI)
 done