changeset 1562 | e98c7f6165c9 |
parent 1531 | e5eb247ad13c |
child 3947 | eb707467f8c5 |
--- 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.