src/HOL/Analysis/Weierstrass_Theorems.thy
changeset 68743 91162dd89571
parent 68601 7828f3b85156
child 68833 fde093888c16