Summary
- tuned;
- merged
- added command 'ML_export';
- more examples;
- tuned output;
- pretty-print according to defaults of input syntax;
- more accurate diagram;
- proper output;
The file was modified | src/Doc/Isar_Ref/Spec.thy (diff) |
The file was modified | NEWS (diff) |
The file was modified | src/Doc/Isar_Ref/Spec.thy (diff) |
The file was modified | src/Pure/ML/ml_env.ML (diff) |
The file was modified | src/Pure/Pure.thy (diff) |
The file was modified | src/Doc/System/Environment.thy (diff) |
The file was modified | src/Pure/Isar/element.ML (diff) |
The file was modified | src/Pure/Syntax/mixfix.ML (diff) |
The file was modified | src/Doc/Isar_Ref/Inner_Syntax.thy (diff) |
The file was modified | src/Pure/Syntax/mixfix.ML (diff) |