src/HOLCF/Pcpodef.thy
changeset 26027 87cb69d27558
parent 25926 aa0eca1ccb19
child 26420 57a626f64875
     1.1 --- a/src/HOLCF/Pcpodef.thy	Thu Jan 31 21:37:20 2008 +0100
     1.2 +++ b/src/HOLCF/Pcpodef.thy	Thu Jan 31 21:48:14 2008 +0100
     1.3 @@ -151,7 +151,7 @@
     1.4   apply (rule contI)
     1.5   apply (simp only: typedef_thelub [OF type less adm])
     1.6   apply (simp only: Abs_inverse_lub_Rep [OF type less adm])
     1.7 - apply (rule thelubE [OF _ refl])
     1.8 + apply (rule cpo_lubI)
     1.9   apply (erule ch2ch_Rep [OF less])
    1.10  done
    1.11