src/HOL/Analysis/Elementary_Metric_Spaces.thy
changeset 78943 bc89bdc65f29
parent 78890 d8045bc0544e
child 79772 817d33f8aa7f