src/HOL/Arith.thy
changeset 4271 3a82492e70c5
parent 3366 2402c6ab1561
child 4360 40e5c97e988d