src/HOL/Algebra/Ring_Divisibility.thy
changeset 72567 aeac6424d3b5
parent 70160 8e9100dcde52
child 80914 d97fdabd9e2b