src/HOL/NatDef.thy
changeset 10618 5b96bc5fbec3
parent 10212 33fe2d701ddd
child 10832 e33b47e4246d