Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. X = trivial_topology rather than topspace X = {}
  2. merged
  3. trivial_topology
Changeset 78338:c4cc276821d4 by paulson _lp15@cam.ac.uk_:
X = trivial_topology rather than topspace X = {}
The file was modified NEWS (diff)
Changeset 78337:1d71ceb76e06 by paulson:
merged
Changeset 78336:6bae28577994 by paulson _lp15@cam.ac.uk_:
trivial_topology
The file was modified src/HOL/Analysis/Abstract_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Abstract_Metric_Spaces.thy (diff)
The file was modified src/HOL/Analysis/Abstract_Topological_Spaces.thy (diff)
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/Function_Topology.thy (diff)
The file was modified src/HOL/Analysis/Further_Topology.thy (diff)
The file was modified src/HOL/Analysis/Homotopy.thy (diff)
The file was modified src/HOL/Analysis/Lindelof_Spaces.thy (diff)
The file was modified src/HOL/Analysis/Locally.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Product_Topology.thy (diff)
The file was modified src/HOL/Analysis/Retracts.thy (diff)
The file was modified src/HOL/Analysis/T1_Spaces.thy (diff)
The file was modified src/HOL/Analysis/Urysohn.thy (diff)
The file was modified src/HOL/Homology/Homology_Groups.thy (diff)
The file was modified src/HOL/Homology/Invariance_of_Domain.thy (diff)
The file was modified src/HOL/Homology/Simplices.thy (diff)