src/HOL/Algebra/RingHom.thy
changeset 23112 2bc882fbe51c
parent 21502 7f3ea2b3bab6
child 23350 50c5b0912a0c