Summary
- merged
- tuned proof
- more robust pretty printing of broken YXML, e.g. single "\^E";
The file was modified | src/HOL/Data_Structures/RBT_Set2.thy (diff) |
The file was modified | src/Pure/ML/ml_syntax.ML (diff) |
The file was modified | src/Pure/PIDE/yxml.ML (diff) |