src/HOL/Computational_Algebra/Factorial_Ring.thy
changeset 69272 15e9ed5b28fb
parent 68606 96a49db47c97
child 69785 9e326f6f8a24