![[Jenkins]](/jenkins/static/858a1f95/images/svgs/logo.svg){kind=logo}
Summary
- session containing computational algebra
- more approproiate placement of theories MiscAlgebra and Multiplicate_Group
| The file was added | src/HOL/Computational_Algebra/Computational_Algebra.thy |
| The file was added | src/HOL/Computational_Algebra/Euclidean_Algorithm.thy |
| The file was added | src/HOL/Computational_Algebra/Factorial_Ring.thy |
| The file was added | src/HOL/Computational_Algebra/Field_as_Ring.thy |
| The file was added | src/HOL/Computational_Algebra/Formal_Power_Series.thy |
| The file was added | src/HOL/Computational_Algebra/Fraction_Field.thy |
| The file was added | src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy |
| The file was added | src/HOL/Computational_Algebra/Normalized_Fraction.thy |
| The file was added | src/HOL/Computational_Algebra/Polynomial.thy |
| The file was added | src/HOL/Computational_Algebra/Polynomial_FPS.thy |
| The file was added | src/HOL/Computational_Algebra/Polynomial_Factorial.thy |
| The file was added | src/HOL/Computational_Algebra/Primes.thy |
| The file was modified | NEWS (diff) |
| The file was modified | src/HOL/Algebra/Exponent.thy (diff) |
| The file was modified | src/HOL/Algebra/IntRing.thy (diff) |
| The file was modified | src/HOL/Analysis/Arcwise_Connected.thy (diff) |
| The file was modified | src/HOL/Codegenerator_Test/Candidates.thy (diff) |
| The file was modified | src/HOL/Isar_Examples/Fibonacci.thy (diff) |
| The file was modified | src/HOL/Library/Library.thy (diff) |
| The file was modified | src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy (diff) |
| The file was modified | src/HOL/Number_Theory/Cong.thy (diff) |
| The file was modified | src/HOL/Number_Theory/Eratosthenes.thy (diff) |
| The file was modified | src/HOL/Proofs/Extraction/Euclid.thy (diff) |
| The file was modified | src/HOL/ROOT (diff) |
| The file was modified | src/HOL/ex/Sqrt.thy (diff) |
| The file was modified | src/HOL/ex/Sqrt_Script.thy (diff) |
| The file was removed | src/HOL/Library/Field_as_Ring.thy |
| The file was removed | src/HOL/Library/Formal_Power_Series.thy |
| The file was removed | src/HOL/Library/Fraction_Field.thy |
| The file was removed | src/HOL/Library/Fundamental_Theorem_Algebra.thy |
| The file was removed | src/HOL/Library/Normalized_Fraction.thy |
| The file was removed | src/HOL/Library/Polynomial.thy |
| The file was removed | src/HOL/Library/Polynomial_FPS.thy |
| The file was removed | src/HOL/Library/Polynomial_Factorial.thy |
| The file was removed | src/HOL/Number_Theory/Euclidean_Algorithm.thy |
| The file was removed | src/HOL/Number_Theory/Factorial_Ring.thy |
| The file was removed | src/HOL/Number_Theory/Primes.thy |
| The file was added | src/HOL/Algebra/More_Finite_Product.thy |
| The file was added | src/HOL/Algebra/More_Group.thy |
| The file was added | src/HOL/Algebra/More_Ring.thy |
| The file was added | src/HOL/Algebra/Multiplicative_Group.thy |
| The file was modified | src/HOL/Number_Theory/Pocklington.thy (diff) |
| The file was modified | src/HOL/Number_Theory/Quadratic_Reciprocity.thy (diff) |
| The file was modified | src/HOL/Number_Theory/Residues.thy (diff) |
| The file was modified | src/HOL/ROOT (diff) |
| The file was removed | src/HOL/Number_Theory/MiscAlgebra.thy |