src/HOL/NatDef.ML
changeset 8843 5370a030dd47
parent 8741 61bc5ed22b62
child 8942 6aad5381ba83