src/ZF/ArithSimp.thy
changeset 41561 d1318f3c86ba
parent 35762 af3ff2ba4c54
child 41777 1f7cbe39d425