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