src/HOL/RealVector.thy
changeset 42082 47f8bfe0f597
parent 41969 1cf3e4107a2a
child 44127 7b57b9295d98
equal deleted inserted replaced
42081:21697a5cb34a 42082:47f8bfe0f597