src/HOL/Analysis/Finite_Cartesian_Product.thy
changeset 69448 51e696887b81
parent 69272 15e9ed5b28fb
child 69517 dc20f278e8f3