src/HOL/RealVector.thy
changeset 30653 fbd548c4bb6a
parent 30273 ecd6f0ca62ea
child 30729 461ee3e49ad3