src/HOL/Orderings.thy
changeset 22473 753123c89d72
parent 22424 8a5412121687
child 22548 6ce4bddf3bcb
     1.1 --- a/src/HOL/Orderings.thy	Mon Mar 19 19:28:27 2007 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Tue Mar 20 08:27:15 2007 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  
     1.5  subsection {* Order syntax *}
     1.6  
     1.7 -class ord =
     1.8 +class ord = type +
     1.9    fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubseteq>" 50)
    1.10      and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubset>" 50)
    1.11  begin