src/HOL/Algebra/RingHom.thy
changeset 33959 2afc55e8ed27
parent 30729 461ee3e49ad3
child 35849 b5522b51cb1e