src/HOL/NatDef.thy
changeset 2647 83c9bdff7fdc
parent 2608 450c9b682a92
child 3236 882e125ed7da