src/HOLCF/Universal.thy
changeset 30729 461ee3e49ad3
parent 30561 5e6088e1d6df
child 31076 99fe356cbbc2
     1.1 --- a/src/HOLCF/Universal.thy	Thu Mar 26 19:24:21 2009 +0100
     1.2 +++ b/src/HOLCF/Universal.thy	Thu Mar 26 20:08:55 2009 +0100
     1.3 @@ -230,13 +230,13 @@
     1.4  apply (simp add: ubasis_take_same)
     1.5  done
     1.6  
     1.7 -interpretation udom!: preorder ubasis_le
     1.8 +interpretation udom: preorder ubasis_le
     1.9  apply default
    1.10  apply (rule ubasis_le_refl)
    1.11  apply (erule (1) ubasis_le_trans)
    1.12  done
    1.13  
    1.14 -interpretation udom!: basis_take ubasis_le ubasis_take
    1.15 +interpretation udom: basis_take ubasis_le ubasis_take
    1.16  apply default
    1.17  apply (rule ubasis_take_less)
    1.18  apply (rule ubasis_take_idem)
    1.19 @@ -285,7 +285,7 @@
    1.20  unfolding udom_principal_def
    1.21  by (simp add: Abs_udom_inverse udom.ideal_principal)
    1.22  
    1.23 -interpretation udom!:
    1.24 +interpretation udom:
    1.25    ideal_completion ubasis_le ubasis_take udom_principal Rep_udom
    1.26  apply unfold_locales
    1.27  apply (rule ideal_Rep_udom)