src/HOL/Algebra/RingHom.thy
changeset 35603 c0db094d0d80
parent 30729 461ee3e49ad3
child 35849 b5522b51cb1e