src/HOL/Algebra/poly/PolyHomo.thy
changeset 13145 59bc43b51aa2
parent 11779 1aa328cb273a
child 13735 7de9342aca7a