src/HOL/RealVector.thy
changeset 37979 0f21ebea4a73
parent 37887 2ae085b07f2f
child 38621 d6cb7e625d75
equal deleted inserted replaced
37978:548f3f165d05 37979:0f21ebea4a73