src/HOL/Conditionally_Complete_Lattices.thy
changeset 65466 b0f89998c2a1
parent 63540 f8652d0534fa
child 67091 1393c2340eec
     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Wed Apr 12 09:27:43 2017 +0200
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Wed Apr 12 09:27:47 2017 +0200
     1.3 @@ -10,12 +10,19 @@
     1.4  imports Finite_Set Lattices_Big Set_Interval
     1.5  begin
     1.6  
     1.7 -lemma (in linorder) Sup_fin_eq_Max: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X"
     1.8 +context linorder
     1.9 +begin
    1.10 +  
    1.11 +lemma Sup_fin_eq_Max:
    1.12 +  "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X"
    1.13    by (induct X rule: finite_ne_induct) (simp_all add: sup_max)
    1.14  
    1.15 -lemma (in linorder) Inf_fin_eq_Min: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf_fin X = Min X"
    1.16 +lemma Inf_fin_eq_Min:
    1.17 +  "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf_fin X = Min X"
    1.18    by (induct X rule: finite_ne_induct) (simp_all add: inf_min)
    1.19  
    1.20 +end
    1.21 +
    1.22  context preorder
    1.23  begin
    1.24