Summary
- merged
- more abstract Export.Provider;
- clarified signature: persistent results;
- tuned signature;
- tuned def. of del and proved preservation of rbt (finally)
The file was modified | src/Pure/Thy/export.scala (diff) |
The file was modified | src/Pure/Thy/export_theory.scala (diff) |
The file was modified | src/Pure/PIDE/document.scala (diff) |
The file was modified | src/Pure/Tools/dump.scala (diff) |
The file was modified | src/HOL/Data_Structures/RBT_Map.thy (diff) |