src/HOL/Analysis/Bounded_Continuous_Function.thy
changeset 69506 7d59af98af29
parent 69260 0a9688695a1b
child 69861 62e47f06d22c