src/HOLCF/UpperPD.thy
changeset 29237 e90d9d51106b
parent 27405 785f5dbec8f4
child 29244 95d591908d8d
     1.1 --- a/src/HOLCF/UpperPD.thy	Tue Dec 16 15:09:37 2008 +0100
     1.2 +++ b/src/HOLCF/UpperPD.thy	Tue Dec 16 21:10:53 2008 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOLCF/UpperPD.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Brian Huffman
     1.7  *)
     1.8  
     1.9 @@ -27,7 +26,7 @@
    1.10  apply (erule (1) trans_less)
    1.11  done
    1.12  
    1.13 -interpretation upper_le: preorder [upper_le]
    1.14 +interpretation upper_le!: preorder upper_le
    1.15  by (rule preorder.intro, rule upper_le_refl, rule upper_le_trans)
    1.16  
    1.17  lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<sharp> t"
    1.18 @@ -132,8 +131,8 @@
    1.19  unfolding upper_principal_def
    1.20  by (simp add: Abs_upper_pd_inverse upper_le.ideal_principal)
    1.21  
    1.22 -interpretation upper_pd:
    1.23 -  ideal_completion [upper_le pd_take upper_principal Rep_upper_pd]
    1.24 +interpretation upper_pd!:
    1.25 +  ideal_completion upper_le pd_take upper_principal Rep_upper_pd
    1.26  apply unfold_locales
    1.27  apply (rule pd_take_upper_le)
    1.28  apply (rule pd_take_idem)
    1.29 @@ -249,7 +248,7 @@
    1.30  apply (simp add: PDPlus_absorb)
    1.31  done
    1.32  
    1.33 -interpretation aci_upper_plus: ab_semigroup_idem_mult ["op +\<sharp>"]
    1.34 +interpretation aci_upper_plus!: ab_semigroup_idem_mult "op +\<sharp>"
    1.35    by unfold_locales
    1.36      (rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+
    1.37