src/HOL/NatDef.thy
changeset 3225 cee363fc07d7
parent 2608 450c9b682a92
child 3236 882e125ed7da