Skip to content
Success

Changes

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

Summary

  1. prefer antiquotations;
  2. clarified modules;
  3. more documentation;
  4. merged
  5. tuned whitespace;
  6. clarified signature: File.read_lines is based on scalable Bytes.T; discontinued somewhat pointless File.fold_lines;
  7. clarified modules;
  8. prefer scalable Bytes.T;
  9. unused;
  10. prefer scalable Bytes.T;
Changeset 75621:aeb412065742 by wenzelm:
prefer antiquotations;
The file was modified src/Pure/General/base64.ML
The file was modified src/Pure/General/xz.ML
The file was modified src/Pure/ROOT.ML
Changeset 75620:44815dc2b8f9 by wenzelm:
clarified modules;
The file was addedsrc/Pure/General/base64.ML
The file was addedsrc/Pure/General/base64.scala
The file was addedsrc/Pure/General/xz.ML
The file was modified NEWS
The file was modified etc/build.props
The file was modified src/Pure/General/bytes.scala
The file was modified src/Pure/General/xz.scala
The file was modified src/Pure/ROOT.ML
The file was modified src/Pure/System/isabelle_system.ML
The file was modified src/Pure/System/scala.scala
Changeset 75619:9639c3867b86 by wenzelm:
more documentation;
The file was modified src/Doc/Implementation/ML.thy
Changeset 75618:85a7795675be by wenzelm:
merged
Changeset 75617:be89ec4a4523 by wenzelm:
tuned whitespace;
The file was modified src/Doc/Implementation/ML.thy
Changeset 75616:986506233812 by wenzelm:
clarified signature: File.read_lines is based on scalable Bytes.T;<br>discontinued somewhat pointless File.fold_lines;
The file was modified src/HOL/Import/import_rule.ML
The file was modified src/HOL/TPTP/mash_eval.ML
The file was modified src/HOL/TPTP/mash_export.ML
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
The file was modified src/Pure/General/file.ML
The file was modified src/Tools/cache_io.ML
Changeset 75615:4494cd69f97f by wenzelm:
clarified modules;
The file was addedsrc/Pure/General/file_stream.ML
The file was modified src/HOL/Tools/sat_solver.ML
The file was modified src/Pure/General/bytes.ML
The file was modified src/Pure/General/file.ML
The file was modified src/Pure/PIDE/byte_message.ML
The file was modified src/Pure/PIDE/yxml.ML
The file was modified src/Pure/ROOT.ML
Changeset 75614:01b3da984e55 by wenzelm:
prefer scalable Bytes.T;
The file was modified src/Tools/cache_io.ML
Changeset 75613:1b50bcd108b7 by wenzelm:
unused;
The file was modified src/Pure/General/file.ML
Changeset 75612:03ae0ba2aa9e by wenzelm:
prefer scalable Bytes.T;
The file was modified src/HOL/Import/import_rule.ML
The file was modified src/HOL/TPTP/mash_eval.ML
The file was modified src/HOL/TPTP/mash_export.ML
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

  1. merged
  2. avoid hardwired pdf;
  3. adapted to Isabelle/986506233812;
Changeset 12732:f8a002855e5e by wenzelm:
merged
Changeset 12731:4968f5a0b474 by wenzelm:
avoid hardwired pdf;
The file was modified thys/Rewrite_Properties_Reduction/ROOT
Changeset 12730:256787b32958 by wenzelm:
adapted to Isabelle/986506233812;
The file was modified thys/Affine_Arithmetic/Print.thy
The file was modified thys/Safe_Distance/Evaluation.thy