src/HOL/Analysis/T1_Spaces.thy
changeset 76371 1ac2416e8432
parent 75455 91c16c5ad3e9
child 77935 7f240b0dabd9