Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/Completion.thy
changeset 28053 a2106c0d8c45
parent 27404 62171da527d6
child 28133 218252dfd81e 
--- a/src/HOLCF/Completion.thy	Thu Aug 28 22:08:02 2008 +0200
+++ b/src/HOLCF/Completion.thy	Thu Aug 28 22:08:11 2008 +0200
@@ -243,7 +243,7 @@
  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
@@ -268,7 +268,7 @@
  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
 
@@ -371,7 +371,7 @@
  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)
isabelle