src/HOL/RealVector.thy
changeset 44514 d02b01e5ab8f
parent 44282 f0de18b62d63
child 44571 bd91b77c4cd6