src/HOL/Algebra/Subrings.thy
changeset 69133 22fe10b4c0c6
parent 69122 1b5178abaf97
child 70160 8e9100dcde52