changeset 68188 | 2af1f142f855 |
parent 68074 | 8d50467f7555 |
child 68833 | fde093888c16 |
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Tue May 15 06:23:12 2018 +0200 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Tue May 15 11:33:43 2018 +0200 @@ -10,6 +10,7 @@ L2_Norm "HOL-Library.Numeral_Type" "HOL-Library.Countable_Set" + "HOL-Library.FuncSet" begin subsection \<open>Finite Cartesian products, with indexing and lambdas\<close>