src/HOL/Algebra/poly/PolyHomo.thy
changeset 14722 8e739a6eaf11
parent 13936 d3671b878828
child 17479 68a7acb5f22e