Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. NEWS; tuned comment;
  2. merged
  3. merged
  4. improved platform coverage: macbroy30, macbroy31; slightly improved performance on lxbroy10;
  5. eliminated unused argument;
  6. accomodate Poly/ML repository version, which treats singleton strings as boxed;
  7. re-use "threads" for --gcthreads;
  8. merged
  9. setprod -> prod
  10. merged
  11. Modified transfer principle in HOL/NSA to cause less ho-unficiation
  12. merged
  13. updated to setsum -> sum
  14. setsum -> sum
  15. uniform Isabelle settings -- avoid picking up different JAVA_HOME;
Changeset 64280:7ad033e28dbd by wenzelm:
NEWS;<br>tuned comment;
The file was modified NEWS (diff)
The file was modified src/Pure/General/mercurial.scala (diff)
Changeset 64279:a65ff5a84296 by wenzelm:
merged
Changeset 64278:298a6df049f0 by wenzelm:
merged
Changeset 64277:5ca4ac099e94 by wenzelm:
improved platform coverage: macbroy30, macbroy31;<br>slightly improved performance on lxbroy10;
The file was modified src/Pure/Admin/isabelle_cronjob.scala (diff)
Changeset 64276:622f4e4ac388 by wenzelm:
eliminated unused argument;
The file was modified src/Pure/Concurrent/future.ML (diff)
The file was modified src/Pure/Concurrent/multithreading.ML (diff)
The file was modified src/Pure/Concurrent/single_assignment.ML (diff)
The file was modified src/Pure/Concurrent/synchronized.ML (diff)
Changeset 64275:ac2abc987cf9 by wenzelm:
accomodate Poly/ML repository version, which treats singleton strings as boxed;
The file was modified src/Pure/General/sha1.ML (diff)
The file was modified src/Pure/General/symbol.ML (diff)
The file was modified src/Pure/ML/ml_lex.ML (diff)
The file was modified src/Pure/PIDE/yxml.ML (diff)
The file was modified src/Pure/Syntax/lexicon.ML (diff)
The file was modified src/Pure/library.ML (diff)
Changeset 64274:c8990e5feac9 by wenzelm:
re-use &quot;threads&quot; for --gcthreads;
The file was modified NEWS (diff)
The file was modified src/Pure/Tools/ml_process.scala (diff)
Changeset 64273:2e94501cbc34 by nipkow:
merged
Changeset 64272:f76b6dda2e56 by nipkow:
setprod -&gt; prod
The file was modified src/Doc/Main/Main_Doc.thy (diff)
The file was modified src/HOL/Algebra/IntRing.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/Determinants.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.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/Generalised_Binomial_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Lebesgue_Measure.thy (diff)
The file was modified src/HOL/Analysis/Weierstrass_Theorems.thy (diff)
The file was modified src/HOL/Analysis/ex/Approximations.thy (diff)
The file was modified src/HOL/Binomial.thy (diff)
The file was modified src/HOL/Complex.thy (diff)
The file was modified src/HOL/Decision_Procs/Approximation.thy (diff)
The file was modified src/HOL/Deriv.thy (diff)
The file was modified src/HOL/GCD.thy (diff)
The file was modified src/HOL/Groups_Big.thy (diff)
The file was modified src/HOL/Groups_List.thy (diff)
The file was modified src/HOL/Int.thy (diff)
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy (diff)
The file was modified src/HOL/Library/Extended_Real.thy (diff)
The file was modified src/HOL/Library/Formal_Power_Series.thy (diff)
The file was modified src/HOL/Library/Groups_Big_Fun.thy (diff)
The file was modified src/HOL/Library/Multiset.thy (diff)
The file was modified src/HOL/Library/Multiset_Permutations.thy (diff)
The file was modified src/HOL/Library/Polynomial.thy (diff)
The file was modified src/HOL/Library/Polynomial_FPS.thy (diff)
The file was modified src/HOL/Library/RBT_Set.thy (diff)
The file was modified src/HOL/Lifting_Set.thy (diff)
The file was modified src/HOL/Limits.thy (diff)
The file was modified src/HOL/List.thy (diff)
The file was modified src/HOL/Nat_Transfer.thy (diff)
The file was modified src/HOL/Number_Theory/Cong.thy (diff)
The file was modified src/HOL/Number_Theory/Factorial_Ring.thy (diff)
The file was modified src/HOL/Number_Theory/Gauss.thy (diff)
The file was modified src/HOL/Number_Theory/Primes.thy (diff)
The file was modified src/HOL/Number_Theory/Residues.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Euler.thy (diff)
The file was modified src/HOL/Old_Number_Theory/EulerFermat.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Finite2.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Gauss.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Int2.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Pocklington.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Residues.thy (diff)
The file was modified src/HOL/Old_Number_Theory/WilsonBij.thy (diff)
The file was modified src/HOL/Old_Number_Theory/WilsonRuss.thy (diff)
The file was modified src/HOL/Probability/Central_Limit_Theorem.thy (diff)
The file was modified src/HOL/Probability/Independent_Family.thy (diff)
The file was modified src/HOL/Probability/Infinite_Product_Measure.thy (diff)
The file was modified src/HOL/Probability/Probability_Measure.thy (diff)
The file was modified src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy (diff)
The file was modified src/HOL/Rat.thy (diff)
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)
The file was modified src/HOL/Set_Interval.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)
The file was modified src/HOL/ex/Birthday_Paradox.thy (diff)
The file was modified src/HOL/ex/Sum_of_Powers.thy (diff)
Changeset 64271:912573107a2e by wimmers:
merged
Changeset 64270:bf474d719011 by simon wimmer _wimmers@in.tum.de_:
Modified transfer principle in HOL/NSA to cause less ho-unficiation
The file was modified src/HOL/Nonstandard_Analysis/StarDef.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/transfer.ML (diff)
Changeset 64269:c939cc16b605 by nipkow:
merged
Changeset 64268:3faa948dc861 by nipkow:
updated to setsum -&gt; sum
The file was modified src/Doc/Prog_Prove/Bool_nat_list.thy (diff)
Changeset 64267:b9a1486e79be by nipkow:
setsum -&gt; sum
The file was modified src/Doc/Logics/document/HOL.tex (diff)
The file was modified src/Doc/Main/Main_Doc.thy (diff)
The file was modified src/Doc/Sugar/Sugar.thy (diff)
The file was modified src/HOL/Algebra/IntRing.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/Bounded_Continuous_Function.thy (diff)
The file was modified src/HOL/Analysis/Bounded_Linear_Function.thy (diff)
The file was modified src/HOL/Analysis/Brouwer_Fixpoint.thy (diff)
The file was modified src/HOL/Analysis/Caratheodory.thy (diff)
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Cauchy_Integral_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Complex_Analysis_Basics.thy (diff)
The file was modified src/HOL/Analysis/Complex_Transcendental.thy (diff)
The file was modified src/HOL/Analysis/Conformal_Mappings.thy (diff)
The file was modified src/HOL/Analysis/Continuous_Extension.thy (diff)
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Derivative.thy (diff)
The file was modified src/HOL/Analysis/Determinants.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Fashoda_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Finite_Cartesian_Product.thy (diff)
The file was modified src/HOL/Analysis/Gamma_Function.thy (diff)
The file was modified src/HOL/Analysis/Harmonic_Numbers.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Homeomorphism.thy (diff)
The file was modified src/HOL/Analysis/Inner_Product.thy (diff)
The file was modified src/HOL/Analysis/Integral_Test.thy (diff)
The file was modified src/HOL/Analysis/L2_Norm.thy (diff)
The file was modified src/HOL/Analysis/Lebesgue_Measure.thy (diff)
The file was modified src/HOL/Analysis/Linear_Algebra.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/Ordered_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Poly_Roots.thy (diff)
The file was modified src/HOL/Analysis/Polytope.thy (diff)
The file was modified src/HOL/Analysis/Regularity.thy (diff)
The file was modified src/HOL/Analysis/Summation_Tests.thy (diff)
The file was modified src/HOL/Analysis/Tagged_Division.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Uniform_Limit.thy (diff)
The file was modified src/HOL/Analysis/Weierstrass_Theorems.thy (diff)
The file was modified src/HOL/Analysis/ex/Approximations.thy (diff)
The file was modified src/HOL/Binomial.thy (diff)
The file was modified src/HOL/Complex.thy (diff)
The file was modified src/HOL/Datatype_Examples/Misc_Primrec.thy (diff)
The file was modified src/HOL/Decision_Procs/Approximation.thy (diff)
The file was modified src/HOL/Deriv.thy (diff)
The file was modified src/HOL/Groups_Big.thy (diff)
The file was modified src/HOL/Groups_List.thy (diff)
The file was modified src/HOL/HOLCF/Universal.thy (diff)
The file was modified src/HOL/Hoare_Parallel/OG_Examples.thy (diff)
The file was modified src/HOL/Hoare_Parallel/RG_Examples.thy (diff)
The file was modified src/HOL/IMP/Abs_Int0.thy (diff)
The file was modified src/HOL/IMP/Abs_Int1.thy (diff)
The file was modified src/HOL/IMP/Abs_Int3.thy (diff)
The file was modified src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy (diff)
The file was modified src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy (diff)
The file was modified src/HOL/Inequalities.thy (diff)
The file was modified src/HOL/Int.thy (diff)
The file was modified src/HOL/Library/BigO.thy (diff)
The file was modified src/HOL/Library/Bourbaki_Witt_Fixpoint.thy (diff)
The file was modified src/HOL/Library/Combine_PER.thy (diff)
The file was modified src/HOL/Library/Extended_Nat.thy (diff)
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy (diff)
The file was modified src/HOL/Library/Extended_Real.thy (diff)
The file was modified src/HOL/Library/FSet.thy (diff)
The file was modified src/HOL/Library/Finite_Map.thy (diff)
The file was modified src/HOL/Library/Formal_Power_Series.thy (diff)
The file was modified src/HOL/Library/Groups_Big_Fun.thy (diff)
The file was modified src/HOL/Library/Indicator_Function.thy (diff)
The file was modified src/HOL/Library/Multiset.thy (diff)
The file was modified src/HOL/Library/Multiset_Permutations.thy (diff)
The file was modified src/HOL/Library/Nat_Bijection.thy (diff)
The file was modified src/HOL/Library/Permutations.thy (diff)
The file was modified src/HOL/Library/Polynomial.thy (diff)
The file was modified src/HOL/Library/Polynomial_FPS.thy (diff)
The file was modified src/HOL/Library/Polynomial_Factorial.thy (diff)
The file was modified src/HOL/Library/Product_Plus.thy (diff)
The file was modified src/HOL/Library/RBT_Set.thy (diff)
The file was modified src/HOL/Library/Set_Algebras.thy (diff)
The file was modified src/HOL/Library/Stirling.thy (diff)
The file was modified src/HOL/Lifting_Set.thy (diff)
The file was modified src/HOL/Limits.thy (diff)
The file was modified src/HOL/List.thy (diff)
The file was modified src/HOL/MacLaurin.thy (diff)
The file was modified src/HOL/Metis_Examples/Big_O.thy (diff)
The file was modified src/HOL/Nat_Transfer.thy (diff)
The file was modified src/HOL/Nitpick.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/HSeries.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/Nonstandard_Analysis.thy (diff)
The file was modified src/HOL/NthRoot.thy (diff)
The file was modified src/HOL/Number_Theory/Cong.thy (diff)
The file was modified src/HOL/Number_Theory/Factorial_Ring.thy (diff)
The file was modified src/HOL/Number_Theory/Fib.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Euler.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Fib.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Finite2.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Residues.thy (diff)
The file was modified src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy (diff)
The file was modified src/HOL/Probability/Central_Limit_Theorem.thy (diff)
The file was modified src/HOL/Probability/Characteristic_Functions.thy (diff)
The file was modified src/HOL/Probability/Distributions.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/PMF_Impl.thy (diff)
The file was modified src/HOL/Probability/Probability_Mass_Function.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/SPMF.thy (diff)
The file was modified src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy (diff)
The file was modified src/HOL/Rat.thy (diff)
The file was modified src/HOL/Real.thy (diff)
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)
The file was modified src/HOL/Series.thy (diff)
The file was modified src/HOL/Set_Interval.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)
The file was modified src/HOL/UNITY/Comp/Alloc.thy (diff)
The file was modified src/HOL/UNITY/Comp/AllocBase.thy (diff)
The file was modified src/HOL/UNITY/Comp/AllocImpl.thy (diff)
The file was modified src/HOL/UNITY/Follows.thy (diff)
The file was modified src/HOL/ex/Execute_Choice.thy (diff)
The file was modified src/HOL/ex/HarmonicSeries.thy (diff)
The file was modified src/HOL/ex/Meson_Test.thy (diff)
The file was modified src/HOL/ex/Sum_of_Powers.thy (diff)
The file was modified src/HOL/ex/ThreeDivides.thy (diff)
The file was modified src/HOL/ex/Transfer_Int_Nat.thy (diff)
Changeset 64266:4699d3b3173e by wenzelm:
uniform Isabelle settings -- avoid picking up different JAVA_HOME;
The file was modified Admin/cronjob/main (diff)