src/HOL/RealVector.thy
changeset 31456 55edadbd43d5
parent 31419 74fc28c5d68c
child 31446 2d91b2416de8