Summary
- more direct locale goal: avoid renaming of type_parameters;
- adapted to Library/LaTeXsugar
- const_typ also works for fixed variables - useful primarily for locales
- tuned message according to ML version;
- more liberal: detect free-form infixes as well, e.g. Orderings.ord_class.less_eq;
The file was modified | src/Pure/Thy/export_theory.ML (diff) |
The file was modified | src/Doc/Prog_Prove/LaTeXsugar.thy (diff) |
The file was modified | src/Doc/Sugar/Sugar.thy (diff) |
The file was modified | src/HOL/Library/LaTeXsugar.thy (diff) |
The file was modified | src/Pure/Thy/sessions.scala (diff) |
The file was modified | src/Pure/Syntax/printer.ML (diff) |