src/HOL/Algebra/abstract/RingHomo.thy
changeset 32206 b2e93cda0be8
parent 27541 9e585e99b494
child 35849 b5522b51cb1e