src/HOL/Analysis/Bounded_Continuous_Function.thy
changeset 80451 e0bd9e4811ad
parent 78890 d8045bc0544e
child 80914 d97fdabd9e2b
equal deleted inserted replaced
80450:4355857e13a6 80451:e0bd9e4811ad