src/HOL/RealVector.thy
changeset 50860 e32a283b8ce0
parent 49962 a8cc904a6820
child 50999 3de230ed0547
equal deleted inserted replaced
50859:c0f38015a632 50860:e32a283b8ce0