src/HOL/NatDef.ML
changeset 3362 0b268cff9344
parent 3355 0d955bcf8e0a
child 3378 11f4884a071a