src/HOL/Analysis/Bounded_Continuous_Function.thy
changeset 64492 98215fa4f8d1
parent 64267 b9a1486e79be
child 65036 ab7e11730ad8