src/HOL/Algebra/RingHom.thy
changeset 54257 5c7a3b6b05a9
parent 44655 fe0365331566
child 61169 4de9ff3ea29a