src/HOL/RealVector.thy
changeset 50180 c6626861c31a
parent 49962 a8cc904a6820
child 50999 3de230ed0547
equal deleted inserted replaced
50178:ad52ddd35c3a 50180:c6626861c31a