src/HOL/Library/Finite_Cartesian_Product.thy
changeset 31259 c1b981b71dba
parent 30661 54858c8ad226