src/HOL/NatDef.ML
changeset 8888 343c304e714a
parent 8741 61bc5ed22b62
child 8942 6aad5381ba83