src/HOL/RealVector.thy
changeset 46127 af3b95160b59
parent 44937 22c0857b8aab
child 46868 6c250adbe101
equal deleted inserted replaced
46126:bab00660539d 46127:af3b95160b59