src/HOL/Factorial.thy
changeset 78988 ee8c014526dc
parent 75865 62c64e3e4741
child 79566 f783490c6c99