1.1 --- a/src/HOL/HOL.thy	Fri Sep 28 10:35:53 2007 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat Sep 29 08:58:51 2007 +0200
     1.3 @@ -244,8 +244,8 @@
     1.4    abs  ("\<bar>_\<bar>")
     1.5  
     1.6  class ord = type +
     1.7 -  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubseteq>" 50)
     1.8 -    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubset>" 50)
     1.9 +  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.10 +    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.11  begin
    1.12  
    1.13  notation