src/HOL/NatDef.ML
changeset 3477 3aced7fa7d8b
parent 3457 a8ab7c64817c
child 3484 1e93eb09ebb9