src/HOL/Analysis/Weierstrass_Theorems.thy
changeset 76963 a8566127d43b
parent 76037 f3f1cf4711d7
child 79586 9cde97e471df