src/HOL/Arith.thy
changeset 4447 b7ee449eb345
parent 4360 40e5c97e988d
child 4711 75a9ef36b1fe