src/HOL/Algebra/abstract/RingHomo.ML
changeset 9502 50ec59aff389
parent 8707 5de763446504
child 10448 da7d0e28f746