src/ZF/Order.thy
1994-06-21 lcp 1994-06-21 Addition of cardinals and order types, various tidying