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
```