Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. simplified/clarified persistent session information;
  2. merged
  3. refer to command_timings/last_timing via resources;
  4. more uniform Resources.init_session via YXML;
  5. proper link for Pure;
  6. proper link location;
  7. clarified access to single database server vs. collection of database files;
  8. merged
  9. Multiplicative_Group now required due to Algebra restructuring
  10. merged
  11. Jakub Kądziołka's stronger version of generate_pow_card (required some restructuring)
  12. de-applying and tidying
Changeset 72640:fffad9ad660e by wenzelm:
simplified/clarified persistent session information;
The file was modified src/Pure/PIDE/session.ML (diff)
The file was modified src/Pure/Tools/build.ML (diff)
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 72639:db5f4572704a by wenzelm:
merged
Changeset 72638:2a7fc87495e0 by wenzelm:
refer to command_timings/last_timing via resources;
The file was modified src/Pure/PIDE/resources.ML (diff)
The file was modified src/Pure/PIDE/resources.scala (diff)
The file was modified src/Pure/Thy/thy_info.ML (diff)
The file was modified src/Pure/Tools/build.ML (diff)
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 72637:fd68c9c1b90b by wenzelm:
more uniform Resources.init_session via YXML;
The file was modified src/Pure/ML/ml_process.scala (diff)
The file was modified src/Pure/PIDE/protocol.ML (diff)
The file was modified src/Pure/PIDE/protocol.scala (diff)
The file was modified src/Pure/PIDE/resources.ML (diff)
The file was modified src/Pure/PIDE/resources.scala (diff)
The file was modified src/Pure/Tools/build.ML (diff)
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 72636:09ee9eb7a3d3 by wenzelm:
proper link for Pure;
The file was modified src/Pure/Thy/html.ML (diff)
The file was modified src/Pure/Thy/present.ML (diff)
Changeset 72635:2a329baa7d39 by wenzelm:
proper link location;
The file was modified src/Pure/Thy/present.ML (diff)
Changeset 72634:5cea0993ee4f by wenzelm:
clarified access to single database server vs. collection of database files;
The file was modified src/Pure/Thy/export.scala (diff)
The file was modified src/Pure/Thy/present.scala (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 72633:20f70d20e6f8 by paulson:
merged
Changeset 72632:773ad766f1b8 by paulson _lp15@cam.ac.uk_:
Multiplicative_Group now required due to Algebra restructuring
The file was modified src/HOL/Homology/Brouwer_Degree.thy (diff)
Changeset 72631:bafc0ec0e018 by paulson:
merged
Changeset 72630:4167d3d3d478 by paulson _lp15@cam.ac.uk_:
Jakub Kądziołka's stronger version of generate_pow_card (required some restructuring)
The file was modified CONTRIBUTORS (diff)
The file was modified src/HOL/Algebra/Elementary_Groups.thy (diff)
The file was modified src/HOL/Algebra/Free_Abelian_Groups.thy (diff)
The file was modified src/HOL/Algebra/Multiplicative_Group.thy (diff)
Changeset 72629:a995071b8e6d by paulson _lp15@cam.ac.uk_:
de-applying and tidying
The file was modified src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy (diff)