Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. more database content; clarified signature; tuned comments;
  3. tuned signature;
  4. tuned whitespace;
  5. tuned signature;
  6. merged
  7. More of Eberl's material
  8. Some new lemmas. Some tidying up
  9. detect duplicates in Sledgehammer output -- suggested by Larry Paulson
  10. got rid of 'important message' mechanism in SystemOnTPTP (which is less used nowadays)
Changeset 77497:b9e01beef1c5 by wenzelm:
merged
Changeset 77496:f0d9f9196b9b by wenzelm:
more database content;<br>clarified signature;<br>tuned comments;
The file was modified src/Pure/Tools/build_job.scala (diff)
The file was modified src/Pure/Tools/build_process.scala (diff)
Changeset 77495:c546e3e1f7f6 by wenzelm:
tuned signature;
The file was modified src/Pure/Tools/build_process.scala (diff)
Changeset 77494:1a32b4928aad by wenzelm:
tuned whitespace;
The file was modified src/Pure/Admin/build_log.scala (diff)
Changeset 77493:2d5529f56124 by wenzelm:
tuned signature;
The file was modified src/Pure/Tools/build_job.scala (diff)
Changeset 77492:fd9422c110ed by paulson:
merged
Changeset 77491:9d431c939a7f by paulson _lp15@cam.ac.uk_:
More of Eberl&#039;s material
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Complex_Analysis/Contour_Integration.thy (diff)
The file was modified src/HOL/Library/Landau_Symbols.thy (diff)
The file was modified src/HOL/Series.thy (diff)
Changeset 77490:2c86ea8961b5 by paulson _lp15@cam.ac.uk_:
Some new lemmas. Some tidying up
The file was modified src/HOL/Analysis/Convex.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Metric_Spaces.thy (diff)
The file was modified src/HOL/Analysis/Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Archimedean_Field.thy (diff)
The file was modified src/HOL/Library/Landau_Symbols.thy (diff)
The file was modified src/HOL/Real.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)
Changeset 77489:8a28ab58d155 by blanchet:
detect duplicates in Sledgehammer output -- suggested by Larry Paulson
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)
Changeset 77488:615a6a6a4b0b by blanchet:
got rid of &#039;important message&#039; mechanism in SystemOnTPTP (which is less used nowadays)
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML (diff)