src/HOL/Arith.thy
changeset 3564 f886dbd91ee5
parent 3366 2402c6ab1561
child 4360 40e5c97e988d