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