src/HOL/Analysis/Finite_Cartesian_Product.thy
changeset 81275 5ed639c16ce7
parent 81116 0fb1e2dd4122
child 81471 1b24a570bcf7