| changeset 66453 | cc19f7ca2ed6 |
| parent 66281 | 6ad54b84ca5d |
| child 67155 | 9e5b05d54f9d |
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Fri Aug 18 13:55:05 2017 +0200 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Fri Aug 18 20:47:47 2017 +0200 @@ -8,9 +8,9 @@ imports Euclidean_Space L2_Norm - "~~/src/HOL/Library/Numeral_Type" - "~~/src/HOL/Library/Countable_Set" - "~~/src/HOL/Library/FuncSet" + "HOL-Library.Numeral_Type" + "HOL-Library.Countable_Set" + "HOL-Library.FuncSet" begin subsection \<open>Finite Cartesian products, with indexing and lambdas.\<close>