Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned data structure: potentially more efficient add_prods;
  2. clarified operations;
  3. merged
  4. expand definitions of \DeclareOldFontCommand in traditional article.cls, e.g. KOMA-Script no longer provides these;
Changeset 67530:a7de81d847b0 by wenzelm:
tuned data structure: potentially more efficient add_prods;
The file was modified src/Pure/Syntax/parser.ML (diff)
Changeset 67529:37db2dc5c022 by wenzelm:
clarified operations;
The file was modified src/Pure/General/table.ML (diff)
Changeset 67528:ea029c521b5b by wenzelm:
merged
Changeset 67527:a93a9e89da72 by wenzelm:
expand definitions of \DeclareOldFontCommand in traditional article.cls, e.g. KOMA-Script no longer provides these;
The file was modified lib/texinputs/isabelle.sty (diff)
The file was modified lib/texinputs/isabellesym.sty (diff)