src/HOL/Orderings.thy
changeset 53216 ad2e09c30aa8
parent 53215 5e47c31c6f7c
child 54147 97a8ff4e4ac9
     1.1 --- a/src/HOL/Orderings.thy	Tue Aug 27 14:37:56 2013 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Tue Aug 27 16:06:27 2013 +0200
     1.3 @@ -1230,10 +1230,10 @@
     1.4  
     1.5  subsection {* Dense orders *}
     1.6  
     1.7 -class inner_dense_order = order +
     1.8 +class dense_order = order +
     1.9    assumes dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
    1.10  
    1.11 -class inner_dense_linorder = linorder + inner_dense_order
    1.12 +class dense_linorder = linorder + dense_order
    1.13  begin
    1.14  
    1.15  lemma dense_le:
    1.16 @@ -1312,7 +1312,7 @@
    1.17  class no_bot = order + 
    1.18    assumes lt_ex: "\<exists>y. y < x"
    1.19  
    1.20 -class unbounded_dense_linorder = inner_dense_linorder + no_top + no_bot
    1.21 +class unbounded_dense_linorder = dense_linorder + no_top + no_bot
    1.22  
    1.23  
    1.24  subsection {* Wellorders *}