src/HOL/Algebra/Subrings.thy
changeset 69912 dd55d2c926d9
parent 69122 1b5178abaf97
child 70160 8e9100dcde52