src/HOL/Arith.thy
changeset 5826 977f789566b7
parent 5183 89f162de39cf
child 8929 4829556a56f8