src/ZF/ArithSimp.thy
changeset 74500 40f03761f77f
parent 69605 a96320074298
child 76213 e44d86131648