src/HOL/Library/Uprod.thy
changeset 79025 f78ee2d48bf5
parent 75624 22d1c5f2b9f4