src/HOL/Analysis/Bounded_Continuous_Function.thy
changeset 68970 b0dfe57dfa09
parent 68838 5e013478bced
child 69260 0a9688695a1b