src/HOL/Analysis/Finite_Cartesian_Product.thy
changeset 67333 ac0b81ca3ed5
parent 67155 9e5b05d54f9d
child 67399 eab6ce8368fa