Summary
- Deprivatisation of lemmas in Polynomial_Factorial
- More analysis lemmas
The file was modified | src/HOL/Library/Polynomial_Factorial.thy (diff) |
The file was modified | src/HOL/Analysis/Complex_Transcendental.thy (diff) |
The file was modified | src/HOL/Analysis/Gamma_Function.thy (diff) |
The file was modified | src/HOL/Analysis/Harmonic_Numbers.thy (diff) |
The file was modified | src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff) |
The file was modified | src/HOL/Limits.thy (diff) |
The file was modified | src/HOL/NthRoot.thy (diff) |
The file was modified | src/HOL/Set_Interval.thy (diff) |
The file was modified | src/HOL/Transcendental.thy (diff) |