src/HOL/Arith.thy
changeset 9356 30c3d3e308ee
parent 8970 3ac901561f33
child 9436 62bb04ab4b01