src/HOLCF/LowerPD.thy
changeset 26806 40b411ec05aa
parent 26420 57a626f64875
child 26927 8684b5240f11
     1.1 --- a/src/HOLCF/LowerPD.thy	Wed May 07 10:56:58 2008 +0200
     1.2 +++ b/src/HOLCF/LowerPD.thy	Wed May 07 10:57:19 2008 +0200
     1.3 @@ -106,7 +106,7 @@
     1.4  by (rule Rep_lower_pd [simplified])
     1.5  
     1.6  lemma Rep_lower_pd_mono: "x \<sqsubseteq> y \<Longrightarrow> Rep_lower_pd x \<subseteq> Rep_lower_pd y"
     1.7 -unfolding less_lower_pd_def less_set_def .
     1.8 +unfolding less_lower_pd_def less_set_eq .
     1.9  
    1.10  
    1.11  subsection {* Principal ideals *}
    1.12 @@ -134,12 +134,12 @@
    1.13  apply (rule ideal_Rep_lower_pd)
    1.14  apply (rule cont_Rep_lower_pd)
    1.15  apply (rule Rep_lower_principal)
    1.16 -apply (simp only: less_lower_pd_def less_set_def)
    1.17 +apply (simp only: less_lower_pd_def less_set_eq)
    1.18  done
    1.19  
    1.20  lemma lower_principal_less_iff [simp]:
    1.21    "(lower_principal t \<sqsubseteq> lower_principal u) = (t \<le>\<flat> u)"
    1.22 -unfolding less_lower_pd_def Rep_lower_principal less_set_def
    1.23 +unfolding less_lower_pd_def Rep_lower_principal less_set_eq
    1.24  by (fast intro: lower_le_refl elim: lower_le_trans)
    1.25  
    1.26  lemma lower_principal_mono:
    1.27 @@ -151,7 +151,7 @@
    1.28  apply (simp add: less_lower_pd_def)
    1.29  apply (simp add: cont2contlubE [OF cont_Rep_lower_pd])
    1.30  apply (simp add: Rep_lower_principal set_cpo_simps)
    1.31 -apply (simp add: subset_def)
    1.32 +apply (simp add: subset_eq)
    1.33  apply (drule spec, drule mp, rule lower_le_refl)
    1.34  apply (erule exE, rename_tac i)
    1.35  apply (rule_tac x=i in exI)