src/ZF/ArithSimp.thy
changeset 40750 2064991db2ac
parent 35762 af3ff2ba4c54
child 41777 1f7cbe39d425