Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. clarified signature: tree structure is not essential;
  2. merged
  3. misc tuning and modernization;
  4. merged
  5. use Item_Net to store inductive info
  6. tuned whitespace;
  7. tuned signature;
  8. more accurate qualified lookup; tuned;
  9. clarified fall-back name;
  10. tuned signature;
  11. tuned whitespace;
  12. clarified modules;
  13. clarified checks -- avoid duplicated messages (amending 60c159d490a2);
  14. proper default (amending 601866c61ded);
  15. Fixed import path in Factorial_Ring
  16. Merged
  17. Merged
  18. Tuned
  19. Merged
  20. moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
  21. moved material from AFP to distribution
Changeset 65415:8cd54b18b68b by wenzelm:
clarified signature: tree structure is not essential;
The file was modified Admin/jenkins/build/ci_build_benchmark.scala (diff)
The file was modified Admin/jenkins/build/ci_build_makeall.scala (diff)
The file was modified Admin/jenkins/build/ci_build_makeall_seq.scala (diff)
The file was modified src/Pure/Admin/ci_profile.scala (diff)
The file was modified src/Pure/System/isabelle_process.scala (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Pure/Tools/ml_process.scala (diff)
Changeset 65414:d7ebd2b25b82 by wenzelm:
merged
Changeset 65413:cb7f9d7d35e6 by wenzelm:
misc tuning and modernization;
The file was modified src/HOL/Number_Theory/Gauss.thy (diff)
The file was modified src/HOL/Number_Theory/Quadratic_Reciprocity.thy (diff)
Changeset 65412:da25458453e3 by lars hupel _lars.hupel@mytum.de_:
merged
Changeset 65411:3c628937899d by lars hupel _lars.hupel@mytum.de_:
use Item_Net to store inductive info
The file was modified src/HOL/Library/Countable.thy (diff)
The file was modified src/HOL/Nominal/nominal_inductive.ML (diff)
The file was modified src/HOL/Nominal/nominal_inductive2.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/core_data.ML (diff)
The file was modified src/HOL/Tools/inductive.ML (diff)
The file was modified src/HOL/Tools/inductive_realizer.ML (diff)
Changeset 65410:44253ed65acd by wenzelm:
tuned whitespace;
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 65409:ad9e2c1665b6 by wenzelm:
tuned signature;
The file was modified src/Pure/PIDE/document.scala (diff)
The file was modified src/Pure/PIDE/resources.scala (diff)
Changeset 65408:c728f922f657 by wenzelm:
more accurate qualified lookup;<br>tuned;
The file was modified src/Pure/PIDE/resources.scala (diff)
Changeset 65407:4546272431e9 by wenzelm:
clarified fall-back name;
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Thy/thy_info.scala (diff)
Changeset 65406:cc9e2f1f279d by wenzelm:
tuned signature;
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 65405:68f8a0dab28b by wenzelm:
tuned whitespace;
The file was modified src/Pure/Thy/thy_info.scala (diff)
Changeset 65404:2b819faf45e9 by wenzelm:
clarified modules;
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/Thy/thy_info.scala (diff)
Changeset 65403:4a042bf9488e by wenzelm:
clarified checks -- avoid duplicated messages (amending 60c159d490a2);
The file was modified src/Pure/Thy/thy_info.scala (diff)
Changeset 65402:37d3657e8513 by wenzelm:
proper default (amending 601866c61ded);
The file was modified src/Pure/General/position.scala (diff)
Changeset 65401:590c1a53c78d by eberlm _eberlm@in.tum.de_:
Fixed import path in Factorial_Ring
The file was modified src/HOL/Number_Theory/Factorial_Ring.thy (diff)
Changeset 65400:feb83174a87a by eberlm _eberlm@in.tum.de_:
Merged
Changeset 65399:3f291f7a3646 by eberlm _eberlm@in.tum.de_:
Merged
Changeset 65398:a14fa655b48c by eberlm _eberlm@in.tum.de_:
Tuned
The file was modified src/HOL/Library/Formal_Power_Series.thy (diff)
The file was modified src/HOL/Number_Theory/Euclidean_Algorithm.thy (diff)
The file was modified src/HOL/Number_Theory/Factorial_Ring.thy (diff)
Changeset 65397:9cdafcfb28bf by eberlm _eberlm@in.tum.de_:
Merged
Changeset 65396:b42167902f57 by eberlm _eberlm@in.tum.de_:
moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
The file was modified NEWS (diff)
The file was modified src/HOL/Library/Formal_Power_Series.thy (diff)
Changeset 65395:7504569a73c7 by eberlm _eberlm@in.tum.de_:
moved material from AFP to distribution
The file was modified src/HOL/Analysis/Harmonic_Numbers.thy (diff)
The file was modified src/HOL/Probability/Probability_Mass_Function.thy (diff)
The file was modified src/HOL/Probability/Random_Permutations.thy (diff)