src/HOL/Real/RealVector.thy
changeset 23024 70435ffe077d
parent 22973 64d300e16370
child 23113 d5cdaa3b7517