# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1587333512 -3600
# Node ID af1381b565d692d0814ecf3d914ea0bb1638b5fe
# Parent  7c0de1eb6075cd2ecf270134886bb2cea776a120
Sketch and explore again

diff -r 7c0de1eb6075 -r af1381b565d6 src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Sun Apr 19 22:16:57 2020 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy	Sun Apr 19 22:58:32 2020 +0100
@@ -4,7 +4,6 @@
 
 theory Further_Topology
   imports Weierstrass_Theorems Polytope Complex_Transcendental Equivalence_Lebesgue_Henstock_Integration Retracts
-Sketch_and_Explore
 begin
 
 subsection\<open>A map from a sphere to a higher dimensional sphere is nullhomotopic\<close>