src/HOL/Analysis/Weierstrass_Theorems.thy
changeset 80251 6ae378791c52
parent 80175 200107cdd3ac
child 80521 5c691b178e08