src/HOL/Algebra/RingHom.thy
changeset 21479 63e7eb863ae6
parent 20318 0e0ea63fe768
child 21502 7f3ea2b3bab6