diff -r 9ba6d69f7763 -r e98c7f6165c9 src/HOL/Univ.thy
--- a/src/HOL/Univ.thy	Mon Mar 11 14:04:37 1996 +0100
+++ b/src/HOL/Univ.thy	Mon Mar 11 14:05:45 1996 +0100
@@ -3,8 +3,6 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Move LEAST to Nat.thy???  Could it be defined for all types 'a::ord?
-
 Declares the type 'a node, a subtype of (nat=>nat) * ('a+nat)
 
 Defines "Cartesian Product" and "Disjoint Sum" as set operations.