src/HOL/Computational_Algebra/Factorial_Ring.thy
changeset 77537 1bbf29ec9ce3
parent 76700 c48fe2be847f
child 80084 173548e4d5d0