src/HOL/NatDef.ML
changeset 3942 1f1c1f524d19
parent 3842 b55686a7b22c
child 4000 0614fdf0db20