src/HOLCF/LowerPD.thy

 (*  Title:      HOLCF/LowerPD.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
 header {* Lower powerdomain *}
 

 apply (drule (1) bspec, erule bexE)
 apply (erule rev_bexI)
 apply (erule (1) trans_less)
 done
 
-interpretation lower_le: preorder [lower_le]
+interpretation lower_le!: preorder lower_le
 by (rule preorder.intro, rule lower_le_refl, rule lower_le_trans)
 
 lemma lower_le_minimal [simp]: "PDUnit compact_bot \<le>\<flat> t"
 unfolding lower_le_def Rep_PDUnit
 by (simp, rule Rep_pd_basis_nonempty [folded ex_in_conv])

 lemma Rep_lower_principal:
   "Rep_lower_pd (lower_principal t) = {u. u \<le>\<flat> t}"
 unfolding lower_principal_def
 by (simp add: Abs_lower_pd_inverse lower_le.ideal_principal)
 
-interpretation lower_pd:
-  ideal_completion [lower_le pd_take lower_principal Rep_lower_pd]
+interpretation lower_pd!:
+  ideal_completion lower_le pd_take lower_principal Rep_lower_pd
 apply unfold_locales
 apply (rule pd_take_lower_le)
 apply (rule pd_take_idem)
 apply (erule pd_take_lower_mono)
 apply (rule pd_take_lower_chain)

 lemma lower_plus_absorb: "xs +\<flat> xs = xs"
 apply (induct xs rule: lower_pd.principal_induct, simp)
 apply (simp add: PDPlus_absorb)
 done
 
-interpretation aci_lower_plus: ab_semigroup_idem_mult ["op +\<flat>"]
+interpretation aci_lower_plus!: ab_semigroup_idem_mult "op +\<flat>"
   by unfold_locales
     (rule lower_plus_assoc lower_plus_commute lower_plus_absorb)+
 
 lemma lower_plus_left_commute: "xs +\<flat> (ys +\<flat> zs) = ys +\<flat> (xs +\<flat> zs)"
 by (rule aci_lower_plus.mult_left_commute)