Summary
- misc tuning and modernization;
- more standard notation (like infix);
- dummy fork to produce ML_statistics even in sequential mode (e.g. for heap size);
- expose stderr, e.g. Multithreading.tracing;
- test parallel proof terms in this small session (somewhat slow for bigger applications);
- tuned messages -- more symbols;
- tuned;
- more permissive syntax; more PIDE markup;
The file was modified | src/HOL/Nonstandard_Analysis/CLim.thy (diff) |
The file was modified | src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy (diff) |
The file was modified | src/HOL/Nonstandard_Analysis/StarDef.thy (diff) |
The file was modified | src/Pure/Tools/build.ML (diff) |
The file was modified | src/Pure/Tools/ml_console.scala (diff) |
The file was modified | src/HOL/ROOT (diff) |
The file was modified | src/Pure/Isar/overloading.ML (diff) |
The file was modified | src/Pure/Isar/proof_display.ML (diff) |
The file was modified | src/Pure/primitive_defs.ML (diff) |
The file was modified | src/Pure/Pure.thy (diff) |
The file was modified | src/Pure/ML/ml_antiquotations.ML (diff) |