src/HOL/NatDef.thy
changeset 2981 aa5aeb6467c6
parent 2608 450c9b682a92
child 3236 882e125ed7da