src/HOL/RealVector.thy
changeset 31409 d8537ba165b5
parent 31289 847f00f435d4
child 31413 729d90a531e4