src/HOL/NatDef.ML
changeset 5526 e7617b57a3e6
parent 5500 7e0ed3e31590
child 5591 fbb4e1ac234d