Summary
- merged
- recovered printing of DIM('a) (cf. 899c9c4e4a4c);
- updated;
- simplified syntax;
- clarified syntax category names according to Isabelle/ML/Scala;
- simplified syntax: Parse.term corresponds to Args.term etc.;
- clarified syntax categories;
- cartouche abbreviations work both for " as well;
The file was modified | src/HOL/Multivariate_Analysis/Euclidean_Space.thy (diff) |
The file was modified | src/Doc/Isar_Ref/Outer_Syntax.thy (diff) |
The file was modified | src/Doc/Isar_Ref/Outer_Syntax.thy (diff) |
The file was modified | src/Pure/Isar/parse.ML (diff) |
The file was modified | src/Doc/Isar_Ref/Document_Preparation.thy (diff) |
The file was modified | src/Doc/Isar_Ref/Inner_Syntax.thy (diff) |
The file was modified | src/Doc/Isar_Ref/Outer_Syntax.thy (diff) |
The file was modified | src/Doc/Isar_Ref/Outer_Syntax.thy (diff) |
The file was modified | src/Pure/Isar/parse.ML (diff) |
The file was modified | src/HOL/Tools/Nitpick/nitpick_commands.ML (diff) |
The file was modified | src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML (diff) |
The file was modified | NEWS (diff) |
The file was modified | src/Pure/General/completion.scala (diff) |