src/HOL/Algebra/RingHom.thy
changeset 77901 5728d5ebce34
parent 75963 884dbbc8e1b3