src/HOL/NatDef.ML
changeset 10996 74e970389def
parent 10850 e1a793957a8f
child 11135 8fd0dea26286