Summary
- integrable_spike: new premise order
- merged
- replaced the one use of has_integral_spike_set
- dropping "j < i" condition in lemma
The file was modified | thys/Ordinary_Differential_Equations/ODE_Auxiliarities.thy (diff) |
The file was modified | thys/Stirling_Formula/Ln_Gamma_Asymptotics.thy (diff) |
The file was modified | thys/LLL_Basis_Reduction/LLL_Number_Bounds.thy (diff) |