src/HOL/Algebra/RingHom.thy
changeset 66466 aec5d9c88d69
parent 63167 0909deb8059b
child 67443 3abf6a722518