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