src/HOL/Analysis/Finite_Cartesian_Product.thy
changeset 73934 39e0c7fac69e
parent 71840 8ed78bb0b915
child 73976 a5212df98387
equal deleted inserted replaced
73933:fa92bc604c59 73934:39e0c7fac69e