# HG changeset patch
# User nipkow
# Date 1516631146 -3600
# Node ID c51935a46a8f68aba15f8427a7fae71928d9ea1f
# Parent  aae933ca6fbdf958f1ef646757887c51dce808a9
removed duplicate

diff -r aae933ca6fbd -r c51935a46a8f src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Mon Jan 22 11:23:42 2018 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Mon Jan 22 15:25:46 2018 +0100
@@ -10,19 +10,6 @@
 imports Finite_Set Lattices_Big Set_Interval
 begin
 
-context linorder
-begin
-  
-lemma Sup_fin_eq_Max:
-  "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X"
-  by (induct X rule: finite_ne_induct) (simp_all add: sup_max)
-
-lemma Inf_fin_eq_Min:
-  "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf_fin X = Min X"
-  by (induct X rule: finite_ne_induct) (simp_all add: inf_min)
-
-end
-
 context preorder
 begin
 
@@ -471,10 +458,10 @@
   ..
 
 lemma cSup_eq_Max: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Max X"
-  using cSup_eq_Sup_fin[of X] Sup_fin_eq_Max[of X] by simp
+  using cSup_eq_Sup_fin[of X] by (simp add: Sup_fin_Max)
 
 lemma cInf_eq_Min: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X"
-  using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp
+  using cInf_eq_Inf_fin[of X] by (simp add: Inf_fin_Min)
 
 lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x"
   by (auto intro!: cSup_eq_non_empty intro: dense_le)