src/HOL/Analysis/Weierstrass_Theorems.thy
changeset 79155 53288743c2f0
parent 76037 f3f1cf4711d7
child 79586 9cde97e471df