src/HOL/RealVector.thy
changeset 31488 5691ccb8d6b5
parent 31446 2d91b2416de8
child 31490 c350f3ad6b0d