src/HOL/Univ.thy
changeset 1562 e98c7f6165c9
parent 1531 e5eb247ad13c
child 3947 eb707467f8c5
equal deleted inserted replaced
1561:9ba6d69f7763 1562:e98c7f6165c9
     1 (*  Title:      HOL/Univ.thy
     1 (*  Title:      HOL/Univ.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     4     Copyright   1993  University of Cambridge
     5 
       
     6 Move LEAST to Nat.thy???  Could it be defined for all types 'a::ord?
       
     7 
     5 
     8 Declares the type 'a node, a subtype of (nat=>nat) * ('a+nat)
     6 Declares the type 'a node, a subtype of (nat=>nat) * ('a+nat)
     9 
     7 
    10 Defines "Cartesian Product" and "Disjoint Sum" as set operations.
     8 Defines "Cartesian Product" and "Disjoint Sum" as set operations.
    11 Could <*> be generalized to a general summation (Sigma)?
     9 Could <*> be generalized to a general summation (Sigma)?