src/HOL/RealVector.thy
2008-12-30 ballarin 2008-12-30 Merged.
2008-12-29 haftmann 2008-12-29 adapted HOL source structure to distribution layout