src/HOL/Arith.thy
changeset 1003 6413adca7601
parent 972 e61b058d58d2
child 1370 7361ac9b024d