Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more direct locale goal: avoid renaming of type_parameters;
  2. adapted to Library/LaTeXsugar
  3. const_typ also works for fixed variables - useful primarily for locales
  4. tuned message according to ML version;
  5. more liberal: detect free-form infixes as well, e.g. Orderings.ord_class.less_eq;
Changeset 69083:6f8ae6ddc26b by wenzelm:
more direct locale goal: avoid renaming of type_parameters;
The file was modified src/Pure/Thy/export_theory.ML (diff)
Changeset 69082:0405d06f08f3 by nipkow:
adapted to Library/LaTeXsugar
The file was modified src/Doc/Prog_Prove/LaTeXsugar.thy (diff)
Changeset 69081:0b403ce1e8f8 by nipkow:
const_typ also works for fixed variables - useful primarily for locales
The file was modified src/Doc/Sugar/Sugar.thy (diff)
The file was modified src/HOL/Library/LaTeXsugar.thy (diff)
Changeset 69080:0f1cc8df3409 by wenzelm:
tuned message according to ML version;
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 69079:fedacfd60fdb by wenzelm:
more liberal: detect free-form infixes as well, e.g. Orderings.ord_class.less_eq;
The file was modified src/Pure/Syntax/printer.ML (diff)