src/ZF/ArithSimp.thy
changeset 45107 76fef3e57004
parent 41777 1f7cbe39d425
child 46820 c656222c4dc1