src/HOL/Nat.thy
changeset 5936 406eb27fe53c
parent 5714 b4f2e281a907
child 7702 35c7e0df749f