diff -r 864238c95b56 -r 2f3186b3e455 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Feb 08 15:11:30 2005 +0100
+++ b/src/HOL/Finite_Set.thy	Tue Feb 08 18:32:34 2005 +0100
@@ -2328,7 +2328,8 @@
 done
 
 lemma Lattice_min_max: "Lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
-apply (rule Lattice.intro, simp)
+apply(rule Lattice.intro)
+apply simp
 apply(erule (1) order_trans)
 apply(erule (1) order_antisym)
 apply(simp add:min_def max_def linorder_not_le order_less_imp_le)
@@ -2338,21 +2339,17 @@
 apply(simp add:min_def max_def linorder_not_le order_less_imp_le)
 apply(simp add:min_def max_def linorder_not_le order_less_imp_le)
 apply(rule_tac x=x and y=y in linorder_le_cases)
-apply(rule_tac x=x and y=z in linorder_le_cases)
-apply(rule_tac x=y and y=z in linorder_le_cases)
 apply(simp add:min_def max_def)
 apply(simp add:min_def max_def)
 apply(rule_tac x=y and y=z in linorder_le_cases)
 apply(simp add:min_def max_def)
 apply(simp add:min_def max_def)
-apply(rule_tac x=x and y=z in linorder_le_cases)
-apply(rule_tac x=y and y=z in linorder_le_cases)
-apply(simp add:min_def max_def)
-apply(simp add:min_def max_def)
-apply(rule_tac x=y and y=z in linorder_le_cases)
-apply(simp add:min_def max_def)
-apply(simp add:min_def max_def)
+done
 
+lemma DistribLattice_min_max: "DistribLattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
+apply(rule DistribLattice.intro)
+apply(rule Lattice_min_max)
+apply(rule DistribLattice_axioms.intro)
 apply(rule_tac x=x and y=y in linorder_le_cases)
 apply(rule_tac x=x and y=z in linorder_le_cases)
 apply(rule_tac x=y and y=z in linorder_le_cases)
@@ -2417,11 +2414,9 @@
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A \<le> Max A"
 by(simp add: Min_def Max_def Lattice.Inf_le_Sup[OF Lattice_min_max])
 
-(* FIXME
 lemma max_Min2_distrib:
   "\<lbrakk> finite A; A \<noteq> {}; finite B; B \<noteq> {} \<rbrakk> \<Longrightarrow>
   max (Min A) (Min B) = Min{ max a b |a b. a \<in> A \<and> b \<in> B}"
-by(simp add: Min_def Max_def Lattice.sup_Inf2_distrib[OF Lattice_min_max])
-*)
+by(simp add: Min_def DistribLattice.sup_Inf2_distrib[OF DistribLattice_min_max])
 
 end