# HG changeset patch # User haftmann # Date 1237751171 -3600 # Node ID 88131f2807b6c857e557df8137eb0883c9d2de5b # Parent 254478a8dd05b88ca48bb236fb5e93f0b982457d tuned header diff -r 254478a8dd05 -r 88131f2807b6 src/HOL/Library/Euclidean_Space.thy --- a/src/HOL/Library/Euclidean_Space.thy Sun Mar 22 20:46:11 2009 +0100 +++ b/src/HOL/Library/Euclidean_Space.thy Sun Mar 22 20:46:11 2009 +0100 @@ -5,10 +5,10 @@ header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*} theory Euclidean_Space - imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Complex_Main +imports Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type Inner_Product - uses ("normarith.ML") +uses ("normarith.ML") begin text{* Some common special cases.*}