src/HOL/Arith.thy
changeset 4987 257aeccdefc3
parent 4711 75a9ef36b1fe
child 5183 89f162de39cf