src/ZF/ArithSimp.thy
changeset 11145 3e47692e3a3e
parent 9548 15bee2731e43
child 13259 01fa0c8dbc92