src/HOL/Analysis/T1_Spaces.thy
changeset 76214 0c18df79b1c8
parent 75455 91c16c5ad3e9
child 77935 7f240b0dabd9