| changeset 35028 | 108662d50512 |
| parent 34974 | 18b41bba42b5 |
| child 35092 | cfe605c54e50 |
--- a/src/HOL/Orderings.thy Fri Feb 05 14:33:31 2010 +0100 +++ b/src/HOL/Orderings.thy Fri Feb 05 14:33:50 2010 +0100 @@ -1052,7 +1052,7 @@ subsection {* Dense orders *} -class dense_linear_order = linorder + +class dense_linorder = linorder + assumes gt_ex: "\<exists>y. x < y" and lt_ex: "\<exists>y. y < x" and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"