src/HOL/Algebra/Subrings.thy
changeset 69335 76c8beaf3bab
parent 69122 1b5178abaf97
child 70160 8e9100dcde52