src/ZF/OrderType.thy
Tue, 21 Jun 1994 17:20:34 +0200 lcp Addition of cardinals and order types, various tidying
less more (0) tip