src/ZF/ArithSimp.thy
changeset 59884 bbf49d7dfd6f
parent 58871 c399ae4b836f
child 60770 240563fbf41d