src/HOL/Arith.thy
changeset 7165 8c937127fd8c
parent 5183 89f162de39cf
child 8929 4829556a56f8