src/HOL/NatDef.ML
changeset 7990 0a604b2fc2b1
parent 7064 b053e0ab9f60
child 8555 17325ee838ab