src/HOL/RealVector.thy
changeset 37766 a779f463bae4
parent 36839 34dc65df7014
child 37767 a2b7a20d6ea3
equal deleted inserted replaced
37763:38456e144423 37766:a779f463bae4