Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. tuned proofs --- avoid 'guess';
  3. apply declarations from interpretations in eigen context also
  4. grant access to sun.tools.jconsole, as required for Java 17;
  5. update to e-2.6, following Martin Desharnais;
Changeset 74363:383fd113baae by wenzelm:
merged
Changeset 74362:0135a0c77b64 by wenzelm:
tuned proofs --- avoid 'guess';
The file was modified src/HOL/Analysis/Abstract_Topology_2.thy (diff)
The file was modified src/HOL/Analysis/Binary_Product_Measure.thy (diff)
The file was modified src/HOL/Analysis/Bochner_Integration.thy (diff)
The file was modified src/HOL/Analysis/Borel_Space.thy (diff)
The file was modified src/HOL/Analysis/Caratheodory.thy (diff)
The file was modified src/HOL/Analysis/Complete_Measure.thy (diff)
The file was modified src/HOL/Analysis/Finite_Product_Measure.thy (diff)
The file was modified src/HOL/Analysis/Gamma_Function.thy (diff)
The file was modified src/HOL/Analysis/Interval_Integral.thy (diff)
The file was modified src/HOL/Analysis/Measure_Space.thy (diff)
The file was modified src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy (diff)
The file was modified src/HOL/Analysis/Radon_Nikodym.thy (diff)
The file was modified src/HOL/Analysis/Regularity.thy (diff)
The file was modified src/HOL/Analysis/Set_Integral.thy (diff)
The file was modified src/HOL/Analysis/Sigma_Algebra.thy (diff)
The file was modified src/HOL/Analysis/Summation_Tests.thy (diff)
The file was modified src/HOL/Combinatorics/Multiset_Permutations.thy (diff)
The file was modified src/HOL/Complex_Analysis/Complex_Residues.thy (diff)
The file was modified src/HOL/Computational_Algebra/Factorial_Ring.thy (diff)
The file was modified src/HOL/Computational_Algebra/Formal_Power_Series.thy (diff)
The file was modified src/HOL/Computational_Algebra/Normalized_Fraction.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/Number_Theory/Residue_Primitive_Roots.thy (diff)
The file was modified src/HOL/Probability/Discrete_Topology.thy (diff)
The file was modified src/HOL/Probability/Fin_Map.thy (diff)
The file was modified src/HOL/Probability/Independent_Family.thy (diff)
The file was modified src/HOL/Probability/Information.thy (diff)
The file was modified src/HOL/Probability/Levy.thy (diff)
The file was modified src/HOL/Probability/Probability_Measure.thy (diff)
The file was modified src/HOL/Probability/Projective_Limit.thy (diff)
The file was modified src/HOL/Probability/Stopping_Time.thy (diff)
Changeset 74361:690928dd6f8f by haftmann:
apply declarations from interpretations in eigen context also
The file was modified src/Pure/Isar/generic_target.ML (diff)
Changeset 74360:9e71155e3666 by wenzelm:
grant access to sun.tools.jconsole, as required for Java 17;
The file was modified lib/Tools/java_monitor (diff)
Changeset 74359:8cbe519c2085 by wenzelm:
update to e-2.6, following Martin Desharnais;
The file was modified Admin/components/components.sha1 (diff)
The file was modified Admin/components/main (diff)
The file was modified src/Pure/Admin/build_e.scala (diff)