src/HOL/IMP/Natural.ML
changeset 5330 8c9fadda81f4
parent 5117 7b5efef2ca74
child 5789 7d4ac02677a6