src/HOL/Algebra/poly/PolyHomo.thy
changeset 17184 3d80209e9a53
parent 13936 d3671b878828
child 17479 68a7acb5f22e