1.1 --- a/src/HOLCF/Completion.thy	Thu Aug 28 22:08:02 2008 +0200
     1.2 +++ b/src/HOLCF/Completion.thy	Thu Aug 28 22:08:11 2008 +0200
     1.3 @@ -243,7 +243,7 @@
     1.4   apply (rule is_lub_thelub0)
     1.5    apply (rule basis_fun_lemma0, erule f_mono)
     1.6   apply (rule is_ubI, clarsimp, rename_tac a)
     1.7 - apply (rule sq_le.trans_less [OF f_mono [OF take_chain]])
     1.8 + apply (rule trans_less [OF f_mono [OF take_chain]])
     1.9   apply (rule is_ub_thelub0)
    1.10    apply (rule basis_fun_lemma0, erule f_mono)
    1.11   apply simp
    1.12 @@ -268,7 +268,7 @@
    1.13   apply (rule is_lub_thelub0)
    1.14    apply (rule basis_fun_lemma0, erule f_mono)
    1.15   apply (rule is_ubI, clarsimp, rename_tac a)
    1.16 - apply (rule sq_le.trans_less [OF f_mono [OF take_less]])
    1.17 + apply (rule trans_less [OF f_mono [OF take_less]])
    1.18   apply (erule (1) ub_imageD)
    1.19  done
    1.20  
    1.21 @@ -371,7 +371,7 @@
    1.22   apply (rule is_lub_thelub0)
    1.23    apply (rule basis_fun_lemma, erule f_mono)
    1.24   apply (rule ub_imageI, rename_tac a)
    1.25 - apply (rule sq_le.trans_less [OF less])
    1.26 + apply (rule trans_less [OF less])
    1.27   apply (rule is_ub_thelub0)
    1.28    apply (rule basis_fun_lemma, erule g_mono)
    1.29   apply (erule imageI)