![[Jenkins]](/jenkins/static/98dcae99/images/svgs/logo.svg){kind=logo}
Summary
- consider dvdE for automated classical proving; automatic classical rule to derive a dvd b from b mod a = 0
| The file was modified | thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy (diff) |
| The file was modified | thys/Berlekamp_Zassenhaus/Distinct_Degree_Factorization.thy (diff) |
| The file was modified | thys/Count_Complex_Roots/Extended_Sturm.thy (diff) |
| The file was modified | thys/Fermat3_4/Fermat3.thy (diff) |
| The file was modified | thys/Hoare_Time/QuantK_VCG.thy (diff) |
| The file was modified | thys/Jordan_Normal_Form/Strassen_Algorithm.thy (diff) |
| The file was modified | thys/Polynomial_Factorization/Gauss_Lemma.thy (diff) |
| The file was modified | thys/Rep_Fin_Groups/Rep_Fin_Groups.thy (diff) |
| The file was modified | thys/SumSquares/TwoSquares.thy (diff) |