src/HOL/Analysis/Bounded_Continuous_Function.thy
changeset 65083 9a0e34edfad1
parent 65036 ab7e11730ad8
child 65204 d23eded35a33