src/HOL/Analysis/Continuous_Extension.thy
changeset 67969 83c8cafdebe8
parent 67962 0acdcd8f4ba1
child 67968 a5ad4c015d1c