src/HOL/RealVector.thy
changeset 51523 97b5e8a1291c
parent 51518 6a56b7088a6a