Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. options for process policy, notably for multiprocessor machines;
  2. tuned;
  3. tuned messages -- facilitate copy-paste;
  4. merged
  5. tuned;
  6. tuned proofs;
  7. Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);
  8. clarified lfp/gfp statements and proofs;
  9. repair LaTeX
  10. misc tuning for release;
  11. added lemma;
Changeset 63986:c7a4b03727ae by wenzelm:
options for process policy, notably for multiprocessor machines;
The file was modified NEWS (diff)
The file was modified etc/options (diff)
The file was modified src/Pure/Tools/ml_process.scala (diff)
The file was modified src/Tools/jEdit/lib/Tools/jedit (diff)
The file was modified src/Tools/jEdit/src/jedit_sessions.scala (diff)
Changeset 63985:4effb93c2a09 by wenzelm:
tuned;
The file was modified README_REPOSITORY (diff)
Changeset 63984:6ba87450894d by wenzelm:
tuned messages -- facilitate copy-paste;
The file was modified src/Pure/Tools/build_stats.scala (diff)
Changeset 63983:db9259a5e20e by wenzelm:
merged
Changeset 63982:4c4049e3bad8 by wenzelm:
tuned;
The file was modified src/HOL/Finite_Set.thy (diff)
The file was modified src/HOL/Wellfounded.thy (diff)
Changeset 63981:6f7db4f8df4c by wenzelm:
tuned proofs;
The file was modified src/HOL/Hilbert_Choice.thy (diff)
The file was modified src/HOL/Inductive.thy (diff)
Changeset 63980:f8e556c8ad6f by wenzelm:
Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);
The file was modified src/HOL/BNF_Cardinal_Order_Relation.thy (diff)
The file was modified src/HOL/Hilbert_Choice.thy (diff)
The file was modified src/HOL/Inductive.thy (diff)
The file was modified src/HOL/ROOT (diff)
The file was removedsrc/HOL/Isar_Examples/Schroeder_Bernstein.thy
Changeset 63979:95c3ae4baba8 by wenzelm:
clarified lfp/gfp statements and proofs;
The file was modified NEWS (diff)
The file was modified src/HOL/Complete_Partial_Order.thy (diff)
The file was modified src/HOL/Inductive.thy (diff)
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy (diff)
The file was modified src/HOL/Library/Order_Continuity.thy (diff)
The file was modified src/HOL/Nat.thy (diff)
Changeset 63978:efc958d2fe00 by lars hupel _lars.hupel@mytum.de_:
repair LaTeX
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
Changeset 63977:ec0fb01c6d50 by wenzelm:
misc tuning for release;
The file was modified NEWS (diff)
Changeset 63976:c1a481bb82d3 by wenzelm:
added lemma;
The file was modified src/HOL/Inductive.thy (diff)