src/HOL/Nat.thy
changeset 23555 16e5fd18905c
parent 23476 839db6346cc8
child 23740 d7f18c837ce7