src/HOL/Analysis/Bounded_Continuous_Function.thy
changeset 68915 634768c0bd22
parent 68838 5e013478bced
child 69260 0a9688695a1b