Skip to content
Success

Changes

Summary

  1. new lemmas about segments, etc. Also recast some theorems to use Union rather than general set comprehensions
Changeset 65038:9391ea7daa17 by paulson _lp15@cam.ac.uk_:
new lemmas about segments, etc. Also recast some theorems to use Union rather than general set comprehensions
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)