Skip to content
Failed

Changes

Summary

  1. moved over material from the AFP to HOL, HOL-Computational_Algebra, and HOL-Number_Theory
  2. documented new syntax for fBall and fBex
  3. updated for release;
  4. Added tag Isabelle2024-RC1 for changeset 1231a7fb2510
  5. misc tuning for release;
  6. update for release;
  7. merged
  8. update to stack-2.15.5, stackage-lts-22.15;
  9. clarified names: discontinue odd convention from 3 decades ago;
  10. further performance tuning (after f906f7f83dae): interactive mode is closer to earlier approach with Lazy.value, which could be relevant with rather complex grammars under tight memory situations;
  11. added documentation for meromorphicity etc. in HOL-Complex_Analysis
  12. merged
  13. remove transitional (dummy) component list for Go
Changeset 80808:f48f4303c533 by Manuel Eberl _manuel@pruvisto.org_:
moved over material from the AFP to HOL, HOL-Computational_Algebra, and HOL-Number_Theory
The file was addedsrc/HOL/Algebra/Algebraic_Closure_Type.thy
The file was modified CONTRIBUTORS (diff)
The file was modified src/HOL/Algebra/Algebra.thy (diff)
The file was modified src/HOL/Computational_Algebra/Euclidean_Algorithm.thy (diff)
The file was modified src/HOL/Computational_Algebra/Factorial_Ring.thy (diff)
The file was modified src/HOL/Computational_Algebra/Formal_Laurent_Series.thy (diff)
The file was modified src/HOL/Computational_Algebra/Formal_Power_Series.thy (diff)
The file was modified src/HOL/Computational_Algebra/Polynomial.thy (diff)
The file was modified src/HOL/Computational_Algebra/Polynomial_Factorial.thy (diff)
The file was modified src/HOL/Computational_Algebra/Primes.thy (diff)
The file was modified src/HOL/GCD.thy (diff)
The file was modified src/HOL/Number_Theory/Cong.thy (diff)
The file was modified src/HOL/Number_Theory/Residues.thy (diff)
The file was modified src/HOL/ROOT (diff)
Changeset 80807:1ca617398213 by desharna:
documented new syntax for fBall and fBex
The file was modified NEWS (diff)
Changeset 80806:6e7f266b9ac2 by wenzelm:
updated for release;
The file was modified ANNOUNCE (diff)
Changeset 80805:01ddd3c203da by wenzelm:
Added tag Isabelle2024-RC1 for changeset 1231a7fb2510
The file was modified .hgtags (diff)
Changeset 80804:1231a7fb2510 by wenzelm:
misc tuning for release;
The file was modified NEWS (diff)
Changeset 80803:ee07b7738a24 by wenzelm:
update for release;
The file was modified COPYRIGHT (diff)
Changeset 80802:d67cacd09251 by wenzelm:
merged
Changeset 80801:09e9819beef6 by wenzelm:
update to stack-2.15.5, stackage-lts-22.15;
The file was modified Admin/components/components.sha1 (diff)
The file was modified Admin/components/main (diff)
The file was modified etc/settings (diff)
The file was modified src/Pure/Admin/component_stack.scala (diff)
Changeset 80800:951c371c1cd9 by wenzelm:
clarified names: discontinue odd convention from 3 decades ago;
The file was modified src/Pure/Build/export_theory.ML (diff)
The file was modified src/Pure/Isar/proof_context.ML (diff)
The file was modified src/Pure/Syntax/local_syntax.ML (diff)
The file was modified src/Pure/Syntax/syntax_phases.ML (diff)
The file was modified src/Pure/sign.ML (diff)
The file was modified src/Pure/theory.ML (diff)
Changeset 80799:40f5ddeda2b4 by wenzelm:
further performance tuning (after f906f7f83dae): interactive mode is closer to earlier approach with Lazy.value, which could be relevant with rather complex grammars under tight memory situations;
The file was modified src/Pure/Concurrent/synchronized.ML (diff)
The file was modified src/Pure/Syntax/syntax.ML (diff)
The file was modified src/Pure/System/isabelle_process.ML (diff)
The file was modified src/Pure/theory.ML (diff)
Changeset 80798:33a9b1d6a651 by Manuel Eberl _manuel@pruvisto.org_:
added documentation for meromorphicity etc. in HOL-Complex_Analysis
The file was modified src/HOL/Complex_Analysis/Meromorphic.thy (diff)
Changeset 80797:876bb57e7376 by desharna:
merged
Changeset 80796:d6a787ccf583 by Lars Hupel _lars@hupel.info_:
remove transitional (dummy) component list for Go
The file was removedAdmin/components/go