src/HOL/RealVector.thy
changeset 44631 6820684c7a58
parent 44571 bd91b77c4cd6
child 44937 22c0857b8aab
equal deleted inserted replaced
44630:d08cb39b628a 44631:6820684c7a58