src/HOL/Analysis/Weierstrass_Theorems.thy
changeset 78698 1b9388e6eb75
parent 76037 f3f1cf4711d7
child 79586 9cde97e471df