src/HOL/Analysis/Continuous_Extension.thy
changeset 67728 d97a28a006f9
parent 67613 ce654b0e6d69
child 67962 0acdcd8f4ba1