Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. merged
  2. clarified signature: prefer authentic cterm used in Simplifier, avoid potential re-certification in user-code;
  3. clarified names (see also 9c00a46d69d0, c5cd7a58cf2d); NB: Simplifier.set_trace_ops overrides Pure setup for Simplifier_Trace panel, but that is hardly every used in practice;
  4. provide scala-3.4.1, but do not activate it: scala-3.3.x is LTS version;
  5. clarified "bulky" sessions (again, see also 06153e2e0cdb), but note that "very_slow" is normally used together with "slow";
  6. moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
  7. update NEWS;
  8. moved web_app module from AFP (e.g., for building web services for the distributed build);
  9. added special syntax for FSet.Ball and FSet.Bex
  10. tuned proof
  11. tuned proofs of Equiv_Relations.equiv
Changeset 80795:6de94d690f9f by desharna:
merged
Changeset 80794:60b6c735b5d5 by wenzelm:
clarified signature: prefer authentic cterm used in Simplifier, avoid potential re-certification in user-code;
The file was modified src/Pure/Tools/simplifier_trace.ML (diff)
The file was modified src/Pure/raw_simplifier.ML (diff)
Changeset 80793:0d94dd2fd2d0 by wenzelm:
clarified names (see also 9c00a46d69d0, c5cd7a58cf2d);<br>NB: Simplifier.set_trace_ops overrides Pure setup for Simplifier_Trace panel, but that is hardly every used in practice;
The file was modified src/Pure/Tools/simplifier_trace.ML (diff)
The file was modified src/Pure/raw_simplifier.ML (diff)
Changeset 80792:588ea80f16bb by wenzelm:
provide scala-3.4.1, but do not activate it: scala-3.3.x is LTS version;
The file was modified Admin/components/components.sha1 (diff)
The file was modified src/Pure/Admin/component_scala.scala (diff)
Changeset 80791:1478c6d52864 by wenzelm:
clarified &quot;bulky&quot; sessions (again, see also 06153e2e0cdb), but note that &quot;very_slow&quot; is normally used together with &quot;slow&quot;;
The file was modified src/Pure/Build/sessions.scala (diff)
Changeset 80790:4c1347e172b1 by manuel eberl _eberlm@in.tum.de_:
moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
The file was addedsrc/HOL/Computational_Algebra/document/root.bib
The file was addedsrc/HOL/Computational_Algebra/document/root.tex
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/Fraction_Field.thy (diff)
The file was modified src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy (diff)
The file was modified src/HOL/Computational_Algebra/Polynomial.thy (diff)
The file was modified src/HOL/Groups_List.thy (diff)
The file was modified src/HOL/Library/Multiset.thy (diff)
The file was modified src/HOL/Library/Real_Mod.thy (diff)
The file was modified src/HOL/ROOT (diff)
The file was modified src/HOL/Rat.thy (diff)
Changeset 80789:f82639fe786e by fabian huch _huch@in.tum.de_:
update NEWS;
The file was modified NEWS (diff)
Changeset 80788:37ea0727291f by fabian huch _huch@in.tum.de_:
moved web_app module from AFP (e.g., for building web services for the distributed build);
The file was addedsrc/Pure/System/web_app.scala
The file was modified etc/build.props (diff)
Changeset 80787:67e77f1e6d7b by desharna:
added special syntax for FSet.Ball and FSet.Bex
The file was modified src/HOL/Library/FSet.thy (diff)
Changeset 80786:804a41d08b84 by desharna:
tuned proof
The file was modified src/HOL/Library/Multiset_Order.thy (diff)
Changeset 80771:c40bdfc84640 by desharna:
tuned proofs of Equiv_Relations.equiv
The file was modified src/HOL/Algebra/Coset.thy (diff)
The file was modified src/HOL/Algebra/Sylow.thy (diff)
The file was modified src/HOL/Cardinals/Wellorder_Constructions.thy (diff)
The file was modified src/HOL/Induct/QuoDataType.thy (diff)
The file was modified src/HOL/Induct/QuoNestedDataType.thy (diff)
The file was modified src/HOL/Library/Disjoint_Sets.thy (diff)
The file was modified src/HOL/ZF/Games.thy (diff)