src/HOL/Library/Finite_Cartesian_Product.thy
changeset 31106 9a1178204dc0
parent 30661 54858c8ad226