Summary
- rename f/g_short -> f/g_bound
- merge
- changing heuristic to choose modular factor
The file was modified | thys/LLL_Basis_Reduction/LLL.thy (diff) |
The file was modified | thys/LLL_Factorization/LLL_Factorization.thy (diff) |
The file was modified | thys/LLL_Factorization/LLL_Factorization_Impl.thy (diff) |
The file was modified | thys/LLL_Factorization/Modern_Computer_Algebra_Problem.thy (diff) |