src/HOL/Computational_Algebra/Factorial_Ring.thy
changeset 74671 df12779c3ce8
parent 74542 d592354c4a26
child 74885 2df334453c4c