src/HOL/Algebra/RingHom.thy
changeset 31596 c96d7e5df659
parent 30729 461ee3e49ad3
child 35849 b5522b51cb1e