# HG changeset patch
# User paulson
# Date 826549545 -3600
# Node ID e98c7f6165c9610ef5dd4a8ab6a089139c170488
# Parent  9ba6d69f7763be74d693dd4a1631c9b1ddc63b74
deleted obsolete comment

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.