![[Jenkins]](/jenkins/static/51af4dc4/images/svgs/logo.svg){kind=logo}
Summary
- more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat * * * more rules for setsum, setprod on intervals
- avoid to hide equality behind (output) abbreviation
- default rule for single-step reasoning
| The file was modified | src/HOL/Binomial.thy (diff) |
| The file was modified | src/HOL/Decision_Procs/Approximation.thy (diff) |
| The file was modified | src/HOL/Divides.thy (diff) |
| The file was modified | src/HOL/Library/Formal_Power_Series.thy (diff) |
| The file was modified | src/HOL/Multivariate_Analysis/Gamma.thy (diff) |
| The file was modified | src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy (diff) |
| The file was modified | src/HOL/Multivariate_Analysis/ex/Approximations.thy (diff) |
| The file was modified | src/HOL/NthRoot.thy (diff) |
| The file was modified | src/HOL/Number_Theory/Residues.thy (diff) |
| The file was modified | src/HOL/Power.thy (diff) |
| The file was modified | src/HOL/Set_Interval.thy (diff) |
| The file was modified | src/HOL/Transcendental.thy (diff) |
| The file was modified | src/HOL/ex/Sum_of_Powers.thy (diff) |
| The file was modified | NEWS (diff) |
| The file was modified | src/HOL/Fun.thy (diff) |
| The file was modified | src/HOL/Library/Combine_PER.thy (diff) |