Summary
- Merged
- Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
- Added some simple facts about limits
- added lemmas
The file was modified | src/HOL/Enum.thy (diff) |
The file was modified | src/HOL/Hilbert_Choice.thy (diff) |
The file was modified | src/HOL/Library/Option_ord.thy (diff) |
The file was modified | src/HOL/Predicate.thy (diff) |
The file was modified | src/HOL/Filter.thy (diff) |
The file was modified | src/HOL/Limits.thy (diff) |
The file was modified | src/HOL/Topological_Spaces.thy (diff) |
The file was modified | src/HOL/List.thy (diff) |