src/HOL/Algebra/RingHom.thy
changeset 29667 53103fc8ffa3
parent 29246 3593802c9cf1
child 30729 461ee3e49ad3