src/HOL/RealVector.thy
changeset 38350 480b2de9927c
parent 37887 2ae085b07f2f
child 38621 d6cb7e625d75
equal deleted inserted replaced
38349:ed50e21e715a 38350:480b2de9927c