src/HOL/RealVector.thy
changeset 38566 8176107637ce
parent 37887 2ae085b07f2f
child 38621 d6cb7e625d75