src/HOL/Factorial.thy
changeset 80594 ffef122946a3
parent 79566 f783490c6c99