Skip to content
Failed

Changes

Summary

  1. Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
Changeset 64282:261d42f0bfac by eberlm _eberlm@in.tum.de_:
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
The file was addedsrc/HOL/Number_Theory/Euler_Criterion.thy
The file was addedsrc/HOL/Number_Theory/QuadraticReciprocity.thy
The file was modified src/HOL/Number_Theory/Gauss.thy (diff)
The file was modified src/HOL/Number_Theory/Number_Theory.thy (diff)
The file was modified src/HOL/Number_Theory/Pocklington.thy (diff)
The file was modified src/HOL/Number_Theory/Residues.thy (diff)
The file was modified src/HOL/ROOT (diff)
The file was removedsrc/HOL/Old_Number_Theory/BijectionRel.thy
The file was removedsrc/HOL/Old_Number_Theory/Chinese.thy
The file was removedsrc/HOL/Old_Number_Theory/Euler.thy
The file was removedsrc/HOL/Old_Number_Theory/EulerFermat.thy
The file was removedsrc/HOL/Old_Number_Theory/EvenOdd.thy
The file was removedsrc/HOL/Old_Number_Theory/Factorization.thy
The file was removedsrc/HOL/Old_Number_Theory/Fib.thy
The file was removedsrc/HOL/Old_Number_Theory/Finite2.thy
The file was removedsrc/HOL/Old_Number_Theory/Gauss.thy
The file was removedsrc/HOL/Old_Number_Theory/Int2.thy
The file was removedsrc/HOL/Old_Number_Theory/IntFact.thy
The file was removedsrc/HOL/Old_Number_Theory/IntPrimes.thy
The file was removedsrc/HOL/Old_Number_Theory/Legacy_GCD.thy
The file was removedsrc/HOL/Old_Number_Theory/Pocklington.thy
The file was removedsrc/HOL/Old_Number_Theory/Primes.thy
The file was removedsrc/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
The file was removedsrc/HOL/Old_Number_Theory/Residues.thy
The file was removedsrc/HOL/Old_Number_Theory/WilsonBij.thy
The file was removedsrc/HOL/Old_Number_Theory/WilsonRuss.thy
The file was removedsrc/HOL/Old_Number_Theory/document/root.bib
The file was removedsrc/HOL/Old_Number_Theory/document/root.tex