src/HOL/Orderings.thy
changeset 29823 0ab754d13ccd
parent 29580 117b88da143c
child 30107 f3b3b0e3d184
     1.1 --- a/src/HOL/Orderings.thy	Fri Feb 06 15:15:27 2009 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Fri Feb 06 15:15:32 2009 +0100
     1.3 @@ -1033,7 +1033,6 @@
     1.4    assumes gt_ex: "\<exists>y. x < y" 
     1.5    and lt_ex: "\<exists>y. y < x"
     1.6    and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
     1.7 -  (*see further theory Dense_Linear_Order*)
     1.8  
     1.9  
    1.10  subsection {* Wellorders *}