src/HOL/Algebra/RingHom.thy
changeset 29138 661a8db7e647
parent 28823 dcbef866c9e2
child 29237 e90d9d51106b