![[Jenkins]](/jenkins/static/98dcae99/images/svgs/logo.svg){kind=logo}
Summary
- merged
- Fixes for 91e451bc0f1f. (For simprule status of exp_of_nat_mult and removal of powr_divide2)
| The file was modified | thys/Affine_Arithmetic/Float_Real.thy (diff) |
| The file was modified | thys/Akra_Bazzi/Akra_Bazzi.thy (diff) |
| The file was modified | thys/Akra_Bazzi/Akra_Bazzi_Asymptotics.thy (diff) |
| The file was modified | thys/Akra_Bazzi/Akra_Bazzi_Method.thy (diff) |
| The file was modified | thys/Akra_Bazzi/Master_Theorem.thy (diff) |
| The file was modified | thys/Ergodic_Theory/Fekete.thy (diff) |
| The file was modified | thys/Ergodic_Theory/SG_Library_Complement.thy (diff) |
| The file was modified | thys/Girth_Chromatic/Girth_Chromatic.thy (diff) |
| The file was modified | thys/Landau_Symbols/Landau_Real_Products.thy (diff) |
| The file was modified | thys/Landau_Symbols/Landau_Symbols_Definition.thy (diff) |
| The file was modified | thys/Lp/Lp.thy (diff) |
| The file was modified | thys/Random_Graph_Subgraph_Threshold/Subgraph_Threshold.thy (diff) |
| The file was modified | thys/Stirling_Formula/Stirling_Formula.thy (diff) |