src/HOL/RealVector.thy
changeset 49222 cbe8c859817c
parent 47108 2a1953f0d20d
child 49962 a8cc904a6820
equal deleted inserted replaced
49221:6d8d5fe9f3a2 49222:cbe8c859817c