src/HOL/RealVector.thy
changeset 45261 8716790fe5a3
parent 44937 22c0857b8aab
child 46868 6c250adbe101
equal deleted inserted replaced
45260:48295059cef3 45261:8716790fe5a3