Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. moved generalized lemmas
  2. generalized
  3. split off Homotopy.thy
  4. split off Convex.thy: material that does not require Topology_Euclidean_Space
  5. moved setdist to more appropriate places
  6. reduced dependencies of Connected.thy
  7. split off theory combining Elementary_Topology and Abstract_Topology
  8. moved material from Connected.thy to more appropriate places
  9. generalized
  10. moved material from Connected.thy to more appropriate places
  11. generalized
Changeset 69622:003475955593 by immler:
moved generalized lemmas
The file was modified src/HOL/Analysis/Abstract_Topology.thy (diff)
The file was modified src/HOL/Analysis/Abstract_Topology_2.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Metric_Spaces.thy (diff)
Changeset 69621:9c22ff18125b by immler:
generalized
The file was modified src/HOL/Analysis/Elementary_Metric_Spaces.thy (diff)
Changeset 69620:19d8a59481db by immler:
split off Homotopy.thy
The file was addedsrc/HOL/Analysis/Homotopy.thy
The file was modified src/HOL/Analysis/Brouwer_Fixpoint.thy (diff)
The file was modified src/HOL/Analysis/Homeomorphism.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
Changeset 69619:3f7d8e05e0f2 by immler:
split off Convex.thy: material that does not require Topology_Euclidean_Space
The file was addedsrc/HOL/Analysis/Convex.thy
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Further_Topology.thy (diff)
The file was modified src/HOL/Analysis/Linear_Algebra.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
Changeset 69618:2be1baf40351 by immler:
moved setdist to more appropriate places
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Metric_Spaces.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
Changeset 69617:63ee37c519a3 by immler:
reduced dependencies of Connected.thy
The file was modified src/HOL/Analysis/Connected.thy (diff)
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Normed_Spaces.thy (diff)
The file was modified src/HOL/Analysis/Tagged_Division.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
Changeset 69616:d18dc9c5c456 by immler:
split off theory combining Elementary_Topology and Abstract_Topology
The file was addedsrc/HOL/Analysis/Abstract_Topology_2.thy
The file was modified src/HOL/Analysis/Connected.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Metric_Spaces.thy (diff)
Changeset 69615:e502cd4d7062 by immler:
moved material from Connected.thy to more appropriate places
The file was modified src/HOL/Analysis/Connected.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Metric_Spaces.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Normed_Spaces.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Topology.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
Changeset 69614:d469a1340e21 by immler:
generalized
The file was modified src/HOL/Analysis/Connected.thy (diff)
Changeset 69613:1331e57b54c6 by immler:
moved material from Connected.thy to more appropriate places
The file was modified src/HOL/Analysis/Connected.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Metric_Spaces.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Normed_Spaces.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Topology.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
Changeset 69612:d692ef26021e by immler:
generalized
The file was modified src/HOL/Analysis/Connected.thy (diff)