src/HOL/RealVector.thy
changeset 37136 e0c9d3e49e15
parent 36839 34dc65df7014
child 37767 a2b7a20d6ea3
equal deleted inserted replaced
37135:636e6d8645d6 37136:e0c9d3e49e15