src/HOL/Library/Finite_Cartesian_Product.thy
changeset 30072 4eecd8b9b6cf
parent 29906 80369da39838
child 30267 171b3bd93c90
child 30304 d8e4cd2ac2a1