src/HOL/RealVector.thy
changeset 37742 d8e7f473c3a1
parent 36839 34dc65df7014
child 37767 a2b7a20d6ea3