diff -r ec11275fb263 -r 57bb7da5c867 src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Wed Dec 02 19:14:57 2015 +0100
+++ b/src/HOL/Lattices_Big.thy	Wed Dec 02 19:14:57 2015 +0100
@@ -314,36 +314,18 @@
 context semilattice_inf
 begin
 
-definition Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
-where
-  "Inf_fin = semilattice_set.F inf"
-
 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 .
-  from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule
-qed
+defines
+  Inf_fin ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900) = Inf_fin.F ..
 
 end
 
 context semilattice_sup
 begin
 
-definition Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
-where
-  "Sup_fin = semilattice_set.F sup"
-
 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 .
-  from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule
-qed
+defines
+  Sup_fin ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900) = Sup_fin.F ..
 
 end
 
@@ -482,27 +464,10 @@
 context linorder
 begin
 
-definition Min :: "'a set \<Rightarrow> 'a"
-where
-  "Min = semilattice_set.F min"
-
-definition Max :: "'a set \<Rightarrow> 'a"
-where
-  "Max = semilattice_set.F max"
-
 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 .
-  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 .
-  from Min_def show "semilattice_set.F min = Min" by rule
-  from Max_def show "semilattice_set.F max = Max" by rule
-qed
+defines
+  Min = Min.F and Max = Max.F ..
 
 end