src/HOL/Nat.thy
changeset 7257 745cfc8871e2
parent 5714 b4f2e281a907
child 7702 35c7e0df749f