src/HOL/Algebra/RingHom.thy
changeset 29609 a010aab5bed0
parent 29246 3593802c9cf1
child 30729 461ee3e49ad3