Sketch and explore again
authorpaulson <lp15@cam.ac.uk>
Sun, 19 Apr 2020 22:58:32 +0100
changeset 71772 af1381b565d6
parent 71771 7c0de1eb6075
child 71773 7c2f4dd48fb6
Sketch and explore again
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>