src/HOLCF/Up.thy
changeset 29530 9905b660612b
parent 29138 661a8db7e647
child 31076 99fe356cbbc2
     1.1 --- a/src/HOLCF/Up.thy	Wed Jan 14 13:47:14 2009 -0800
     1.2 +++ b/src/HOLCF/Up.thy	Wed Jan 14 17:11:29 2009 -0800
     1.3 @@ -282,10 +282,10 @@
     1.4  text {* properties of fup *}
     1.5  
     1.6  lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>"
     1.7 -by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo)
     1.8 +by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo cont2cont_LAM)
     1.9  
    1.10  lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x"
    1.11 -by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2)
    1.12 +by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_LAM)
    1.13  
    1.14  lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
    1.15  by (cases x, simp_all)