src/HOL/Computational_Algebra/Factorial_Ring.thy
changeset 78600 afb83ba8d24c
parent 76700 c48fe2be847f
child 80084 173548e4d5d0