src/HOL/Real/RealVector.thy
changeset 25343 31c55418de5a
parent 25062 af5ef0d4d655
child 25571 c9e39eafc7a0