src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
changeset 41413 64cd30d6b0b8
parent 39302 d7728f65b353
child 42290 b1f544c84040
     1.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Dec 29 13:51:17 2010 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Dec 29 17:34:41 2010 +0100
     1.3 @@ -5,7 +5,10 @@
     1.4  header {* Definition of finite Cartesian product types. *}
     1.5  
     1.6  theory Finite_Cartesian_Product
     1.7 -imports Inner_Product L2_Norm Numeral_Type
     1.8 +imports
     1.9 +  "~~/src/HOL/Library/Inner_Product"
    1.10 +  L2_Norm
    1.11 +  "~~/src/HOL/Library/Numeral_Type"
    1.12  begin
    1.13  
    1.14  subsection {* Finite Cartesian products, with indexing and lambdas. *}