deleted obsolete comment
authorpaulson
Mon Mar 11 14:05:45 1996 +0100 (1996-03-11)
changeset 1562e98c7f6165c9
parent 1561 9ba6d69f7763
child 1563 717f8816eca5
deleted obsolete comment
src/HOL/Univ.thy
     1.1 --- a/src/HOL/Univ.thy	Mon Mar 11 14:04:37 1996 +0100
     1.2 +++ b/src/HOL/Univ.thy	Mon Mar 11 14:05:45 1996 +0100
     1.3 @@ -3,8 +3,6 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1993  University of Cambridge
     1.6  
     1.7 -Move LEAST to Nat.thy???  Could it be defined for all types 'a::ord?
     1.8 -
     1.9  Declares the type 'a node, a subtype of (nat=>nat) * ('a+nat)
    1.10  
    1.11  Defines "Cartesian Product" and "Disjoint Sum" as set operations.