Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. Resolved codegen problem with uniformity for formal Laurent series
  2. Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
  3. Exponentiation by squaring, fast modular exponentiation
  4. more thorough File.set_executable, notably for Windows;
  5. added executable flag for exports; clarified signature;
  6. clarified URL -- avoid odd certificate problem with api.media.atlassian.com;
  7. back to stable polyml-5.7.1-8 for now;
  8. More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Changeset 69792:d21789843f01 by manuel eberl _eberlm@in.tum.de_:
Resolved codegen problem with uniformity for formal Laurent series
The file was modified src/HOL/Computational_Algebra/Formal_Laurent_Series.thy (diff)
Changeset 69791:195aeee8b30a by manuel eberl _eberlm@in.tum.de_:
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
The file was addedsrc/HOL/Computational_Algebra/Formal_Laurent_Series.thy
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)
The file was modified src/HOL/Computational_Algebra/Computational_Algebra.thy (diff)
The file was modified src/HOL/Computational_Algebra/Formal_Power_Series.thy (diff)
The file was modified src/HOL/Fields.thy (diff)
The file was modified src/HOL/Int.thy (diff)
The file was modified src/HOL/Orderings.thy (diff)
The file was modified src/HOL/Power.thy (diff)
Changeset 69790:154cf64e403e by manuel eberl _eberlm@in.tum.de_:
Exponentiation by squaring, fast modular exponentiation
The file was addedsrc/HOL/Library/Power_By_Squaring.thy
The file was addedsrc/HOL/Number_Theory/Mod_Exp.thy
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)
The file was modified src/HOL/Library/Library.thy (diff)
The file was modified src/HOL/Number_Theory/Number_Theory.thy (diff)
Changeset 69789:2c3e5e58d93f by wenzelm:
more thorough File.set_executable, notably for Windows;
The file was modified src/Pure/Admin/build_cygwin.scala (diff)
The file was modified src/Pure/Admin/build_release.scala (diff)
The file was modified src/Pure/General/file.scala (diff)
The file was modified src/Pure/Thy/export.scala (diff)
Changeset 69788:c175499a7537 by wenzelm:
added executable flag for exports;<br>clarified signature;
The file was modified src/Pure/General/file.scala (diff)
The file was modified src/Pure/PIDE/markup.ML (diff)
The file was modified src/Pure/PIDE/markup.scala (diff)
The file was modified src/Pure/Thy/export.ML (diff)
The file was modified src/Pure/Thy/export.scala (diff)
Changeset 69787:60b5a4731695 by wenzelm:
clarified URL -- avoid odd certificate problem with api.media.atlassian.com;
The file was modified src/Pure/Admin/afp.scala (diff)
Changeset 69786:a5732629cc46 by wenzelm:
back to stable polyml-5.7.1-8 for now;
The file was modified Admin/components/main (diff)
Changeset 69785:9e326f6f8a24 by manuel eberl _eberlm@in.tum.de_:
More material for HOL-Number_Theory: ord, Carmichael&#039;s function, primitive roots
The file was addedsrc/HOL/Number_Theory/Residue_Primitive_Roots.thy
The file was addedsrc/HOL/Number_Theory/document/root.bib
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)
The file was modified src/HOL/Algebra/Multiplicative_Group.thy (diff)
The file was modified src/HOL/Computational_Algebra/Factorial_Ring.thy (diff)
The file was modified src/HOL/Divides.thy (diff)
The file was modified src/HOL/GCD.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/Number_Theory/Totient.thy (diff)
The file was modified src/HOL/Number_Theory/document/root.tex (diff)