src/HOL/Real_Vector_Spaces.thy
changeset 55487 6380313b8ed5
parent 54890 cb892d835803
child 55719 cdddd073bff8
equal deleted inserted replaced
55486:8609527278f2 55487:6380313b8ed5