src/HOL/Algebra/Subrings.thy
changeset 77775 3cc55085d490
parent 73932 fd21b4a93043