src/HOL/Algebra/poly/PolyHomo.thy
changeset 14024 213dcc39358f
parent 13936 d3671b878828
child 17479 68a7acb5f22e