diff -r 23a8c5ac35f8 -r 69916a850301 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/SetInterval.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -1,7 +1,7 @@
 (*  Title:      HOL/SetInterval.thy
-    Author:     Tobias Nipkow and Clemens Ballarin
-                Additions by Jeremy Avigad in March 2004
-    Copyright   2000  TU Muenchen
+    Author:     Tobias Nipkow
+    Author:     Clemens Ballarin
+    Author:     Jeremy Avigad
 
 lessThan, greaterThan, atLeast, atMost and two-sided intervals
 *)
@@ -15,19 +15,19 @@
 context ord
 begin
 definition
-  lessThan    :: "'a => 'a set"	("(1{..<_})") where
+  lessThan    :: "'a => 'a set" ("(1{..<_})") where
   "{..<u} == {x. x < u}"
 
 definition
-  atMost      :: "'a => 'a set"	("(1{.._})") where
+  atMost      :: "'a => 'a set" ("(1{.._})") where
   "{..u} == {x. x \<le> u}"
 
 definition
-  greaterThan :: "'a => 'a set"	("(1{_<..})") where
+  greaterThan :: "'a => 'a set" ("(1{_<..})") where
   "{l<..} == {x. l<x}"
 
 definition
-  atLeast     :: "'a => 'a set"	("(1{_..})") where
+  atLeast     :: "'a => 'a set" ("(1{_..})") where
   "{l..} == {x. l\<le>x}"
 
 definition