| changeset 29823 | 0ab754d13ccd |
| parent 29580 | 117b88da143c |
| child 30107 | f3b3b0e3d184 |
--- a/src/HOL/Orderings.thy Fri Feb 06 15:15:27 2009 +0100 +++ b/src/HOL/Orderings.thy Fri Feb 06 15:15:32 2009 +0100 @@ -1033,7 +1033,6 @@ 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)" - (*see further theory Dense_Linear_Order*) subsection {* Wellorders *}