src/HOL/Analysis/Continuous_Extension.thy
changeset 68743 91162dd89571
parent 68607 67bb59e49834
child 69286 e4d5a07fecb6
equal deleted inserted replaced
68739:0c62e3b4f4c0 68743:91162dd89571