src/HOL/Hahn_Banach/Subspace.thy
changeset 63992 3aa9837d05c7
parent 63910 e4fdf9580372
child 66453 cc19f7ca2ed6
equal deleted inserted replaced
63991:0d8cd1f3c26d 63992:3aa9837d05c7