src/ZF/ArithSimp.thy
changeset 38846 e54c33dbe77c
parent 35762 af3ff2ba4c54
child 41777 1f7cbe39d425