src/HOL/Analysis/T1_Spaces.thy
changeset 69981 3dced198b9ec
parent 69939 812ce526da33
child 69986 f2d327275065