src/HOL/NatDef.ML
changeset 5707 b0e631634b5a
parent 5654 8b872d546b9e
child 5983 79e301a6a51b