src/HOL/Univ.thy
changeset 1562 e98c7f6165c9
parent 1531 e5eb247ad13c
child 3947 eb707467f8c5
     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.