src/HOL/Analysis/Continuous_Extension.thy
changeset 68031 eda52f4cd4e4
parent 67968 a5ad4c015d1c
child 68224 1f7308050349
equal deleted inserted replaced
68028:1f9f973eed2a 68031:eda52f4cd4e4