src/HOL/Algebra/abstract/RingHomo.thy
changeset 31232 689aa7da48cc
parent 27541 9e585e99b494
child 35849 b5522b51cb1e