src/HOL/Computational_Algebra/Factorial_Ring.thy
changeset 82276 d22e9c5b5dc6
parent 80084 173548e4d5d0