src/HOL/Analysis/Continuous_Extension.thy
changeset 68666 4bee4828cfc3
parent 68607 67bb59e49834
child 69286 e4d5a07fecb6
equal deleted inserted replaced
68661:5820f0f379ae 68666:4bee4828cfc3