src/HOL/Algebra/Ring_Divisibility.thy
changeset 72222 01397b6e5eb0
parent 70160 8e9100dcde52
child 80914 d97fdabd9e2b