src/HOL/Algebra/RingHom.thy
changeset 35387 4356263e0bdd
parent 30729 461ee3e49ad3
child 35849 b5522b51cb1e