src/HOL/Orderings.thy
changeset 21194 7e48158e50f6
parent 21180 f27f12bcafb8
child 21204 1e96553668c6
equal deleted inserted replaced
21193:25a5ab43a5ff 21194:7e48158e50f6
    11 
    11 
    12 section {* Abstract orderings *}
    12 section {* Abstract orderings *}
    13 
    13 
    14 subsection {* Order signatures *}
    14 subsection {* Order signatures *}
    15 
    15 
    16 class ord = eq +
    16 class ord =
    17   constrains eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (*FIXME: class_package should do the job*)
       
    18   fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    17   fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    19   fixes less    :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    18   fixes less    :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    20 
    19 
    21 const_syntax
    20 const_syntax
    22   less  ("op <")
    21   less  ("op <")