src/HOL/RealVector.thy
changeset 30988 b53800e3ee47
parent 30729 461ee3e49ad3
child 31017 2c227493ea56
equal deleted inserted replaced
30987:2bbc22bd6a95 30988:b53800e3ee47