src/HOL/Analysis/Finite_Cartesian_Product.thy
changeset 82313 df99e867c63e
parent 81472 e43bff789ac0
child 82967 73af47bc277c