src/HOL/Algebra/poly/PolyHomo.thy
changeset 9502 50ec59aff389
parent 9279 fb4186e20148
child 11093 62c2e0af1d30