Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. discontinued raw symbols; discontinued Symbol.source; use initial Symbol.explode;
  3. raw control symbols are superseded by Latex.embed_raw;
  4. \<^raw> output is intended for LaTeX;
  5. more general mixfix delimiters;
  6. more tight implementation of symbol explode operation (without support for raw symbols);
Changeset 63937:45ed7d0aeb6f by wenzelm:
merged
Changeset 63936:b87784e19a77 by wenzelm:
discontinued raw symbols;<br>discontinued Symbol.source;<br>use initial Symbol.explode;
The file was modified NEWS (diff)
The file was modified src/Doc/Implementation/ML.thy (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_util.ML (diff)
The file was modified src/Pure/General/symbol.ML (diff)
The file was modified src/Pure/General/symbol.scala (diff)
The file was modified src/Pure/General/symbol_explode.ML (diff)
The file was modified src/Pure/Isar/outer_syntax.ML (diff)
The file was modified src/Pure/Isar/token.ML (diff)
The file was modified src/Pure/ML/ml_lex.ML (diff)
The file was modified src/Pure/Thy/latex.ML (diff)
The file was modified src/Pure/Thy/thy_header.ML (diff)
Changeset 63935:aa1fe1103ab8 by wenzelm:
raw control symbols are superseded by Latex.embed_raw;
The file was modified NEWS (diff)
The file was modified src/Doc/Main/Main_Doc.thy (diff)
The file was modified src/Doc/Prog_Prove/Bool_nat_list.thy (diff)
The file was modified src/Doc/Prog_Prove/LaTeXsugar.thy (diff)
The file was modified src/Doc/Prog_Prove/Logic.thy (diff)
The file was modified src/HOL/Library/LaTeXsugar.thy (diff)
The file was modified src/HOL/Library/OptionalSugar.thy (diff)
The file was modified src/HOL/Set_Interval.thy (diff)
The file was modified src/Pure/Thy/latex.ML (diff)
Changeset 63934:397b25cee74c by wenzelm:
\&lt;^raw&gt; output is intended for LaTeX;
The file was modified src/Pure/Thy/html.ML (diff)
Changeset 63933:e149e3e320a3 by wenzelm:
more general mixfix delimiters;
The file was modified NEWS (diff)
The file was modified src/Doc/Isar_Ref/Inner_Syntax.thy (diff)
The file was modified src/Pure/Syntax/syntax_ext.ML (diff)
Changeset 63932:6040db6b929d by wenzelm:
more tight implementation of symbol explode operation (without support for raw symbols);
The file was addedsrc/Pure/General/symbol_explode.ML
The file was modified src/Pure/ROOT.ML (diff)