src/HOL/IMP/Natural.ML
changeset 9927 7a9652294fe0
parent 9556 dcdcfb0545e0