src/ZF/OrderArith.thy
1994-11-29 ago replaced "rules" by "defs"
1994-06-23 ago modifications for cardinal arithmetic