src/HOL/Orderings.thy
changeset 53215 5e47c31c6f7c
parent 52729 412c9e0381a1
child 53216 ad2e09c30aa8
     1.1 --- a/src/HOL/Orderings.thy	Mon Aug 26 23:39:53 2013 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Tue Aug 27 14:37:56 2013 +0200
     1.3 @@ -1312,7 +1312,7 @@
     1.4  class no_bot = order + 
     1.5    assumes lt_ex: "\<exists>y. y < x"
     1.6  
     1.7 -class dense_linorder = inner_dense_linorder + no_top + no_bot
     1.8 +class unbounded_dense_linorder = inner_dense_linorder + no_top + no_bot
     1.9  
    1.10  
    1.11  subsection {* Wellorders *}