src/HOL/Algebra/Ideal_Product.thy
changeset 81483 7d4df25af572
parent 81438 95c9af7483b1