src/HOL/Analysis/Weierstrass_Theorems.thy
changeset 77095 4c2aaf60c22c
parent 76037 f3f1cf4711d7
child 79586 9cde97e471df