Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Changes from Mercurial (hg https://bitbucket.org/isa-afp/afp-devel/ default)

Summary

  1. back to normal;
  2. prefer standard theory name;
Changeset 8528:4da49daadc02 by wenzelm:
back to normal;
The file was modified thys/Ordinary_Differential_Equations/ROOT
Changeset 8527:8b398dbd8b99 by wenzelm:
prefer standard theory name;
The file was modified thys/Applicative_Lifting/Applicative_PMF.thy
The file was modified thys/Buffons_Needle/Buffons_Needle.thy
The file was modified thys/Density_Compiler/Density_Predicates.thy
The file was modified thys/Ergodic_Theory/SG_Library_Complement.thy
The file was modified thys/Fisher_Yates/Fisher_Yates.thy
The file was modified thys/Girth_Chromatic/Girth_Chromatic.thy
The file was modified thys/List_Update/Prob_Theory.thy
The file was modified thys/MFMC_Countable/MFMC_Misc.thy
The file was modified thys/Markov_Models/Markov_Models_Auxiliary.thy
The file was modified thys/Monad_Normalisation/Monad_Normalisation.thy
The file was modified thys/Monomorphic_Monad/Monomorphic_Monad.thy
The file was modified thys/Probabilistic_System_Zoo/Probabilistic_Hierarchy.thy
The file was modified thys/Probabilistic_While/Bernoulli.thy
The file was modified thys/Quick_Sort_Cost/Randomised_Quick_Sort.thy
The file was modified thys/Random_Graph_Subgraph_Threshold/Prob_Lemmas.thy
The file was modified thys/Random_Graph_Subgraph_Threshold/Ugraph_Misc.thy
The file was modified thys/Randomised_Social_Choice/Lotteries.thy
The file was modified thys/Randomised_Social_Choice/Social_Decision_Schemes.thy
The file was modified thys/Randomised_Social_Choice/Stochastic_Dominance.thy
The file was modified thys/Randomised_Social_Choice/Utility_Functions.thy
The file was modified thys/UpDown_Scheme/Grid_Point.thy
The file was modified thys/UpDown_Scheme/Triangular_Function.thy

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

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
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
Changeset 66996:22ca0f37f491 by wenzelm:
delegate boundary cases to existing IntInf.pow;
The file was modified src/Pure/General/integer.ML
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
The file was modified src/Pure/Admin/build_log.scala
Changeset 66994:38fd865aae45 by wenzelm:
tuned (non-unique example);
The file was modified NEWS
Changeset 66993:2c2a346cfe70 by wenzelm:
clarified situation of global theory names;
The file was modified NEWS
The file was modified src/Doc/System/Sessions.thy
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
The file was modified src/HOL/ROOT
The file was modified src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy
The file was modified src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy
The file was modified src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy
The file was modified src/HOL/SPARK/Examples/Sqrt/Sqrt.thy
The file was modified src/HOL/SPARK/Manual/Complex_Types.thy
The file was modified src/HOL/SPARK/Manual/Proc1.thy
The file was modified src/HOL/SPARK/Manual/Proc2.thy
The file was modified src/HOL/SPARK/Manual/Reference.thy
The file was modified src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy