src/HOL/Computational_Algebra/Factorial_Ring.thy
changeset 71751 abf3e80bd815
parent 71398 e0237f2eb49d
child 73103 b69fd6e19662