src/HOL/Algebra/RingHom.thy
changeset 29270 0eade173f77e
parent 29246 3593802c9cf1
child 30729 461ee3e49ad3