src/HOL/Nat.thy
changeset 15130 dc6be28d7f4e
parent 14740 c8e1937110c2
child 15131 c69542757a4d