src/HOL/Arith.thy
changeset 4521 c7f56322a84b
parent 4360 40e5c97e988d
child 4711 75a9ef36b1fe