src/HOL/Analysis/Finite_Cartesian_Product.thy
changeset 68743 91162dd89571
parent 68188 2af1f142f855
child 68833 fde093888c16