src/HOLCF/LowerPD.thy
changeset 30729 461ee3e49ad3
parent 29990 b11793ea15a3
child 31076 99fe356cbbc2
     1.1 --- a/src/HOLCF/LowerPD.thy	Thu Mar 26 19:24:21 2009 +0100
     1.2 +++ b/src/HOLCF/LowerPD.thy	Thu Mar 26 20:08:55 2009 +0100
     1.3 @@ -26,7 +26,7 @@
     1.4  apply (erule (1) trans_less)
     1.5  done
     1.6  
     1.7 -interpretation lower_le!: preorder lower_le
     1.8 +interpretation lower_le: preorder lower_le
     1.9  by (rule preorder.intro, rule lower_le_refl, rule lower_le_trans)
    1.10  
    1.11  lemma lower_le_minimal [simp]: "PDUnit compact_bot \<le>\<flat> t"
    1.12 @@ -133,7 +133,7 @@
    1.13  unfolding lower_principal_def
    1.14  by (simp add: Abs_lower_pd_inverse lower_le.ideal_principal)
    1.15  
    1.16 -interpretation lower_pd!:
    1.17 +interpretation lower_pd:
    1.18    ideal_completion lower_le pd_take lower_principal Rep_lower_pd
    1.19  apply unfold_locales
    1.20  apply (rule pd_take_lower_le)