src/HOL/Lattices_Big.thy
changeset 61605 1bf7b186542e
parent 61566 c3d6e570ccef
child 61776 57bb7da5c867
     1.1 --- a/src/HOL/Lattices_Big.thy	Mon Nov 09 13:49:56 2015 +0100
     1.2 +++ b/src/HOL/Lattices_Big.thy	Mon Nov 09 15:48:17 2015 +0100
     1.3 @@ -318,12 +318,12 @@
     1.4  where
     1.5    "Inf_fin = semilattice_set.F inf"
     1.6  
     1.7 -sublocale Inf_fin!: semilattice_order_set inf less_eq less
     1.8 +sublocale Inf_fin: semilattice_order_set inf less_eq less
     1.9  rewrites
    1.10    "semilattice_set.F inf = Inf_fin"
    1.11  proof -
    1.12    show "semilattice_order_set inf less_eq less" ..
    1.13 -  then interpret Inf_fin!: semilattice_order_set inf less_eq less .
    1.14 +  then interpret Inf_fin: semilattice_order_set inf less_eq less .
    1.15    from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule
    1.16  qed
    1.17  
    1.18 @@ -336,12 +336,12 @@
    1.19  where
    1.20    "Sup_fin = semilattice_set.F sup"
    1.21  
    1.22 -sublocale Sup_fin!: semilattice_order_set sup greater_eq greater
    1.23 +sublocale Sup_fin: semilattice_order_set sup greater_eq greater
    1.24  rewrites
    1.25    "semilattice_set.F sup = Sup_fin"
    1.26  proof -
    1.27    show "semilattice_order_set sup greater_eq greater" ..
    1.28 -  then interpret Sup_fin!: semilattice_order_set sup greater_eq greater .
    1.29 +  then interpret Sup_fin: semilattice_order_set sup greater_eq greater .
    1.30    from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule
    1.31  qed
    1.32  
    1.33 @@ -490,16 +490,16 @@
    1.34  where
    1.35    "Max = semilattice_set.F max"
    1.36  
    1.37 -sublocale Min!: semilattice_order_set min less_eq less
    1.38 -  + Max!: semilattice_order_set max greater_eq greater
    1.39 +sublocale Min: semilattice_order_set min less_eq less
    1.40 +  + Max: semilattice_order_set max greater_eq greater
    1.41  rewrites
    1.42    "semilattice_set.F min = Min"
    1.43    and "semilattice_set.F max = Max"
    1.44  proof -
    1.45    show "semilattice_order_set min less_eq less" by standard (auto simp add: min_def)
    1.46 -  then interpret Min!: semilattice_order_set min less_eq less .
    1.47 +  then interpret Min: semilattice_order_set min less_eq less .
    1.48    show "semilattice_order_set max greater_eq greater" by standard (auto simp add: max_def)
    1.49 -  then interpret Max!: semilattice_order_set max greater_eq greater .
    1.50 +  then interpret Max: semilattice_order_set max greater_eq greater .
    1.51    from Min_def show "semilattice_set.F min = Min" by rule
    1.52    from Max_def show "semilattice_set.F max = Max" by rule
    1.53  qed
    1.54 @@ -530,14 +530,14 @@
    1.55  lemma dual_Min:
    1.56    "linorder.Min greater_eq = Max"
    1.57  proof -
    1.58 -  interpret dual!: linorder greater_eq greater by (fact dual_linorder)
    1.59 +  interpret dual: linorder greater_eq greater by (fact dual_linorder)
    1.60    show ?thesis by (simp add: dual.Min_def dual_min Max_def)
    1.61  qed
    1.62  
    1.63  lemma dual_Max:
    1.64    "linorder.Max greater_eq = Min"
    1.65  proof -
    1.66 -  interpret dual!: linorder greater_eq greater by (fact dual_linorder)
    1.67 +  interpret dual: linorder greater_eq greater by (fact dual_linorder)
    1.68    show ?thesis by (simp add: dual.Max_def dual_max Min_def)
    1.69  qed
    1.70