src/HOL/Computational_Algebra/Factorial_Ring.thy
changeset 82775 61c39a9e5415
parent 80084 173548e4d5d0