src/HOL/Analysis/Continuous_Extension.thy
changeset 69467 e8893c893241
parent 69286 e4d5a07fecb6
child 69508 2a4c8a2a3f8e