src/HOL/Factorial.thy
changeset 69272 15e9ed5b28fb
parent 69182 2424301cc73d
child 70113 c8deb8ba6d05