Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more symbolic latex_output via XML (using YXML within text);
  2. tuned signature: remove unused;
  3. prefer symbolic Latex.environment (typeset in Isabelle/Scala);
  4. tuned signature;
  5. clarified corner cases of syntax;
  6. clarified Parse.embedded_ml: follow documentation (8baf2e8b16e2);
Changeset 74884:229d7ea628c2 by wenzelm:
more symbolic latex_output via XML (using YXML within text);
The file was modified src/Pure/Thy/latex.ML (diff)
Changeset 74883:f32ac01aef5e by wenzelm:
tuned signature: remove unused;
The file was modified src/Pure/Thy/latex.ML (diff)
Changeset 74882:947bb3e09a88 by wenzelm:
prefer symbolic Latex.environment (typeset in Isabelle/Scala);
The file was modified src/Pure/Thy/document_output.ML (diff)
The file was modified src/Pure/Thy/latex.ML (diff)
The file was modified src/Pure/Tools/rail.ML (diff)
Changeset 74881:1e84ae3e886e by wenzelm:
tuned signature;
The file was modified src/Pure/Thy/latex.ML (diff)
The file was modified src/Pure/pure_syn.ML (diff)
Changeset 74880:944d4d616ca0 by wenzelm:
clarified corner cases of syntax;
The file was modified src/Doc/Implementation/Logic.thy (diff)
The file was modified src/Pure/ML/ml_antiquotations.ML (diff)
Changeset 74879:89c7f74b5ae1 by wenzelm:
clarified Parse.embedded_ml: follow documentation (8baf2e8b16e2);
The file was modified src/Pure/Isar/parse.ML (diff)
The file was modified src/Pure/ML/ml_antiquotations.ML (diff)