src/HOL/Algebra/Ring_Divisibility.thy
changeset 70041 2b23dd163c7f
parent 69597 ff784d5a5bfb
child 70160 8e9100dcde52