Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. support for libgmp on x86_64-darwin;
  2. avoid slow IntInf.pow in Poly/ML 5.7.1 testing version, e.g. relevant for AFP/Lorenz_C0;
  3. delegate boundary cases to existing IntInf.pow;
  4. plain identify job for Isabelle + AFP, independent of any Isabelle technology;
  5. tuned (non-unique example);
  6. clarified situation of global theory names;
  7. less global theories -- avoid confusion about special cases;
Changeset 66998:8905114fd23b by wenzelm:
support for libgmp on x86_64-darwin;
The file was addedAdmin/polyml/NOTES
The file was modified src/Pure/Admin/build_polyml.scala (diff)
The file was removedAdmin/polyml/CHECKLIST
Changeset 66997:17eb23e43630 by wenzelm:
avoid slow IntInf.pow in Poly/ML 5.7.1 testing version, e.g. relevant for AFP/Lorenz_C0;
The file was modified src/Pure/General/integer.ML (diff)
Changeset 66996:22ca0f37f491 by wenzelm:
delegate boundary cases to existing IntInf.pow;
The file was modified src/Pure/General/integer.ML (diff)
Changeset 66995:9cb263dbb2f7 by wenzelm:
plain identify job for Isabelle + AFP, independent of any Isabelle technology;
The file was addedAdmin/cronjob/crontab.lxbroy5
The file was addedAdmin/cronjob/plain_identify
The file was modified Admin/cronjob/README (diff)
The file was modified src/Pure/Admin/build_log.scala (diff)
Changeset 66994:38fd865aae45 by wenzelm:
tuned (non-unique example);
The file was modified NEWS (diff)
Changeset 66993:2c2a346cfe70 by wenzelm:
clarified situation of global theory names;
The file was modified NEWS (diff)
The file was modified src/Doc/System/Sessions.thy (diff)
Changeset 66992:69673025292e by wenzelm:
less global theories -- avoid confusion about special cases;
The file was modified src/HOL/Probability/ex/Measure_Not_CCC.thy (diff)
The file was modified src/HOL/ROOT (diff)
The file was modified src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy (diff)
The file was modified src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy (diff)
The file was modified src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy (diff)
The file was modified src/HOL/SPARK/Examples/Sqrt/Sqrt.thy (diff)
The file was modified src/HOL/SPARK/Manual/Complex_Types.thy (diff)
The file was modified src/HOL/SPARK/Manual/Proc1.thy (diff)
The file was modified src/HOL/SPARK/Manual/Proc2.thy (diff)
The file was modified src/HOL/SPARK/Manual/Reference.thy (diff)
The file was modified src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy (diff)