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