src/HOL/Algebra/RingHom.thy
changeset 44262 355d5438f5fb
parent 35849 b5522b51cb1e
child 44655 fe0365331566