diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Lattices_Big.thy --- a/src/HOL/Lattices_Big.thy Mon Nov 09 13:49:56 2015 +0100 +++ b/src/HOL/Lattices_Big.thy Mon Nov 09 15:48:17 2015 +0100 @@ -318,12 +318,12 @@ where "Inf_fin = semilattice_set.F inf" -sublocale Inf_fin!: semilattice_order_set inf less_eq less +sublocale Inf_fin: semilattice_order_set inf less_eq less rewrites "semilattice_set.F inf = Inf_fin" proof - show "semilattice_order_set inf less_eq less" .. - then interpret Inf_fin!: semilattice_order_set inf less_eq less . + then interpret Inf_fin: semilattice_order_set inf less_eq less . from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule qed @@ -336,12 +336,12 @@ where "Sup_fin = semilattice_set.F sup" -sublocale Sup_fin!: semilattice_order_set sup greater_eq greater +sublocale Sup_fin: semilattice_order_set sup greater_eq greater rewrites "semilattice_set.F sup = Sup_fin" proof - show "semilattice_order_set sup greater_eq greater" .. - then interpret Sup_fin!: semilattice_order_set sup greater_eq greater . + then interpret Sup_fin: semilattice_order_set sup greater_eq greater . from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule qed @@ -490,16 +490,16 @@ where "Max = semilattice_set.F max" -sublocale Min!: semilattice_order_set min less_eq less - + Max!: semilattice_order_set max greater_eq greater +sublocale Min: semilattice_order_set min less_eq less + + Max: semilattice_order_set max greater_eq greater rewrites "semilattice_set.F min = Min" and "semilattice_set.F max = Max" proof - show "semilattice_order_set min less_eq less" by standard (auto simp add: min_def) - then interpret Min!: semilattice_order_set min less_eq less . + then interpret Min: semilattice_order_set min less_eq less . show "semilattice_order_set max greater_eq greater" by standard (auto simp add: max_def) - then interpret Max!: semilattice_order_set max greater_eq greater . + then interpret Max: semilattice_order_set max greater_eq greater . from Min_def show "semilattice_set.F min = Min" by rule from Max_def show "semilattice_set.F max = Max" by rule qed @@ -530,14 +530,14 @@ lemma dual_Min: "linorder.Min greater_eq = Max" proof - - interpret dual!: linorder greater_eq greater by (fact dual_linorder) + interpret dual: linorder greater_eq greater by (fact dual_linorder) show ?thesis by (simp add: dual.Min_def dual_min Max_def) qed lemma dual_Max: "linorder.Max greater_eq = Min" proof - - interpret dual!: linorder greater_eq greater by (fact dual_linorder) + interpret dual: linorder greater_eq greater by (fact dual_linorder) show ?thesis by (simp add: dual.Max_def dual_max Min_def) qed