src/HOL/NatDef.ML
changeset 3721 12409b467fae
parent 3718 d78cf498a88c
child 3768 67f4ac759100