Summary
- renamed the constant "limit" as it is too "generic"
- new material for Analysis
The file was modified | src/HOL/Analysis/Abstract_Limits.thy (diff) |
The file was added | src/HOL/Analysis/Abstract_Limits.thy |
The file was added | src/HOL/Analysis/T1_Spaces.thy |
The file was modified | src/HOL/Analysis/Abstract_Topology.thy (diff) |
The file was modified | src/HOL/Analysis/Analysis.thy (diff) |
The file was modified | src/HOL/Analysis/Function_Topology.thy (diff) |
The file was modified | src/HOL/Analysis/Ordered_Euclidean_Space.thy (diff) |
The file was modified | src/HOL/Library/Equipollence.thy (diff) |