Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. HOL-Probability: use tree datastructure from Libary/Tree; hide left/right/var projections
  2. avoid markup, for the sake of Build_Log.Log_File.parse_props;
  3. more robust: store important meta info before potential failure;
  4. tuned message;
Changeset 66049:d20d5a3bf6cf by hoelzl:
HOL-Probability: use tree datastructure from Libary/Tree; hide left/right/var projections
The file was modified src/HOL/Probability/Tree_Space.thy (diff)
Changeset 66048:d244a895da50 by wenzelm:
avoid markup, for the sake of Build_Log.Log_File.parse_props;
The file was modified src/Pure/Tools/build.ML (diff)
Changeset 66047:3e8a897042d9 by wenzelm:
more robust: store important meta info before potential failure;
The file was modified src/Pure/Admin/isabelle_devel.scala (diff)
Changeset 66046:37226f74f33a by wenzelm:
tuned message;
The file was modified src/Pure/Admin/build_log.scala (diff)