src/HOL/Analysis/Weierstrass_Theorems.thy
changeset 63915 bab633745c7f
parent 63627 6ddb43c6b711
child 63918 6bf55e6e0b75