1.1 --- a/src/HOL/SetInterval.thy	Fri Sep 28 10:35:53 2007 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Sat Sep 29 08:58:51 2007 +0200
     1.3 @@ -17,19 +17,19 @@
     1.4  begin
     1.5  definition
     1.6    lessThan    :: "'a => 'a set"	("(1\<^loc>{..<_})") where
     1.7 -  "\<^loc>{..<u} == {x. x \<sqsubset> u}"
     1.8 +  "\<^loc>{..<u} == {x. x \<^loc>< u}"
     1.9  
    1.10  definition
    1.11    atMost      :: "'a => 'a set"	("(1\<^loc>{.._})") where
    1.12 -  "\<^loc>{..u} == {x. x \<sqsubseteq> u}"
    1.13 +  "\<^loc>{..u} == {x. x \<^loc>\<le> u}"
    1.14  
    1.15  definition
    1.16    greaterThan :: "'a => 'a set"	("(1\<^loc>{_<..})") where
    1.17 -  "\<^loc>{l<..} == {x. l\<sqsubset>x}"
    1.18 +  "\<^loc>{l<..} == {x. l\<^loc><x}"
    1.19  
    1.20  definition
    1.21    atLeast     :: "'a => 'a set"	("(1\<^loc>{_..})") where
    1.22 -  "\<^loc>{l..} == {x. l\<sqsubseteq>x}"
    1.23 +  "\<^loc>{l..} == {x. l\<^loc>\<le>x}"
    1.24  
    1.25  definition
    1.26    greaterThanLessThan :: "'a => 'a => 'a set"  ("(1\<^loc>{_<..<_})") where