src/HOL/NatDef.ML
changeset 3462 3472fa00b1d4
parent 3457 a8ab7c64817c
child 3484 1e93eb09ebb9