Summary
- deleted redundant theorem
- merged
- Rationalisation of complex transcendentals, esp the Arg function
The file was modified | src/HOL/Nonstandard_Analysis/NSA.thy (diff) |
The file was modified | NEWS (diff) |
The file was modified | src/HOL/Analysis/Complex_Transcendental.thy (diff) |
The file was modified | src/HOL/Analysis/Further_Topology.thy (diff) |
The file was modified | src/HOL/Analysis/Inner_Product.thy (diff) |
The file was modified | src/HOL/Archimedean_Field.thy (diff) |
The file was modified | src/HOL/Complex.thy (diff) |
The file was modified | src/HOL/Library/Nonpos_Ints.thy (diff) |
The file was modified | src/HOL/Nonstandard_Analysis/NSComplex.thy (diff) |
The file was modified | src/HOL/Real_Vector_Spaces.thy (diff) |
The file was modified | src/HOL/Series.thy (diff) |
The file was modified | src/HOL/Transcendental.thy (diff) |