src/HOL/Computational_Algebra/Factorial_Ring.thy
changeset 70367 81b65ddac59f
parent 69785 9e326f6f8a24
child 71398 e0237f2eb49d