src/HOL/Real_Vector_Spaces.thy
changeset 67161 b762ed417ed9
parent 67135 1a94352812f4
child 67399 eab6ce8368fa
equal deleted inserted replaced
67160:f37bf261bdf6 67161:b762ed417ed9