src/HOL/RealVector.thy
changeset 37891 c26f9d06e82c
parent 37887 2ae085b07f2f
child 38621 d6cb7e625d75
equal deleted inserted replaced
37890:aae46a9ef66c 37891:c26f9d06e82c