src/HOL/Computational_Algebra/Factorial_Ring.thy
changeset 78577 a945b541efff
parent 76700 c48fe2be847f
child 80084 173548e4d5d0