src/HOL/RealVector.thy
changeset 38294 1bef02e7e1b8
parent 37887 2ae085b07f2f
child 38621 d6cb7e625d75
equal deleted inserted replaced
38293:ddd40349129d 38294:1bef02e7e1b8