Skip to content
Success

Changes

Summary

  1. merged
  2. more abstract Export.Provider;
  3. clarified signature: persistent results;
  4. tuned signature;
  5. tuned def. of del and proved preservation of rbt (finally)
Changeset 68419:a1f43b4f984d by wenzelm:
merged
Changeset 68418:366e43cddd20 by wenzelm:
more abstract Export.Provider;
The file was modified src/Pure/Thy/export.scala (diff)
The file was modified src/Pure/Thy/export_theory.scala (diff)
Changeset 68417:21465884037a by wenzelm:
clarified signature: persistent results;
The file was modified src/Pure/PIDE/document.scala (diff)
Changeset 68416:33114721ac9a by wenzelm:
tuned signature;
The file was modified src/Pure/Tools/dump.scala (diff)
Changeset 68415:d74ba11680d4 by nipkow:
tuned def. of del and proved preservation of rbt (finally)
The file was modified src/HOL/Data_Structures/RBT_Map.thy (diff)