Summary
- HOL-Analysis: move Function Topology from AFP/Ergodict_Theory; HOL-Probability: move Essential Supremum from AFP/Lp
The file was added | src/HOL/Analysis/Function_Topology.thy |
The file was added | src/HOL/Analysis/Further_Topology.thy |
The file was modified | src/HOL/Analysis/Analysis.thy (diff) |
The file was modified | src/HOL/Probability/Probability.thy (diff) |
The file was removed | src/HOL/Analysis/FurtherTopology.thy |