src/HOL/Analysis/Finite_Cartesian_Product.thy
changeset 65568 1070be576372
parent 64267 b9a1486e79be
child 66281 6ad54b84ca5d