src/HOL/Computational_Algebra/Factorial_Ring.thy
changeset 70817 dd675800469d
parent 69785 9e326f6f8a24
child 71398 e0237f2eb49d