src/HOL/Analysis/Weierstrass_Theorems.thy
changeset 79025 f78ee2d48bf5
parent 76037 f3f1cf4711d7
child 79586 9cde97e471df