Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. added glyph from "Deja Vu Sans Mono" font;
  2. tuned messages;
  3. merged
  4. allow TeX comment % in formal comment body, but avoid extra space (cf. d7c6054b2ab1);
  5. tuned;
  6. tuned;
  7. more general error suffixes, e.g. for messages that are broken over several lines;
  8. another Latex error seen in the wild: Undefined control sequence. \isamarkupcancel #1->\xout
  9. clarified default;
  10. clarified formal comments;
  11. prefer formal comments;
  12. added \<^cancel> operator for unused text;
  13. tuned;
  14. restored naming of lemmas after corresponding constants
Changeset 67424:0b691782d6e5 by wenzelm:
added glyph from &quot;Deja Vu Sans Mono&quot; font;
The file was modified Admin/components/components.sha1 (diff)
The file was modified Admin/components/main (diff)
The file was modified NEWS (diff)
The file was modified etc/symbols (diff)
The file was modified lib/fonts/IsabelleText.sfd (diff)
The file was modified lib/fonts/IsabelleTextBold.sfd (diff)
Changeset 67423:8bec22c6b0fb by wenzelm:
tuned messages;
The file was modified src/Pure/Thy/latex.scala (diff)
Changeset 67422:eec44c98d8b3 by wenzelm:
merged
Changeset 67421:c4a10621c72e by wenzelm:
allow TeX comment % in formal comment body, but avoid extra space (cf. d7c6054b2ab1);
The file was modified src/Pure/Thy/thy_output.ML (diff)
Changeset 67420:c4c8787ed669 by wenzelm:
tuned;
The file was modified src/Pure/Thy/present.ML (diff)
Changeset 67419:866b1ad870ac by wenzelm:
tuned;
The file was modified NEWS (diff)
Changeset 67418:5a6ed2e679fb by wenzelm:
more general error suffixes, e.g. for messages that are broken over several lines;
The file was modified src/Pure/Thy/latex.scala (diff)
Changeset 67417:34522db6b85a by wenzelm:
another Latex error seen in the wild:<br>Undefined control sequence.<br>\isamarkupcancel #1-&gt;\xout
The file was modified src/Pure/Thy/latex.scala (diff)
Changeset 67416:efc9ec539224 by wenzelm:
clarified default;
The file was modified lib/texinputs/isabelle.sty (diff)
Changeset 67415:53d0fb1359d4 by wenzelm:
clarified formal comments;
The file was modified src/HOL/Nitpick_Examples/Hotel_Nits.thy (diff)
Changeset 67414:c46b3f9f79ea by wenzelm:
prefer formal comments;
The file was modified src/HOL/Nitpick_Examples/Manual_Nits.thy (diff)
The file was modified src/HOL/Predicate_Compile_Examples/Hotel_Example.thy (diff)
The file was modified src/HOL/Quickcheck_Examples/Hotel_Example.thy (diff)
The file was modified src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy (diff)
Changeset 67413:2555713586c8 by wenzelm:
added \&lt;^cancel&gt; operator for unused text;
The file was modified NEWS (diff)
The file was modified etc/symbols (diff)
The file was modified lib/texinputs/isabelle.sty (diff)
The file was modified lib/texinputs/isabellesym.sty (diff)
The file was modified src/Pure/General/symbol.ML (diff)
The file was modified src/Pure/General/symbol_pos.ML (diff)
The file was modified src/Pure/Syntax/lexicon.ML (diff)
The file was modified src/Pure/Thy/thy_output.ML (diff)
Changeset 67412:8b9d75d8f0b4 by wenzelm:
tuned;
The file was modified src/Pure/Syntax/lexicon.ML (diff)
Changeset 67411:3f4b0c84630f by haftmann:
restored naming of lemmas after corresponding constants
The file was modified src/HOL/Binomial.thy (diff)
The file was modified src/HOL/Computational_Algebra/Formal_Power_Series.thy (diff)
The file was modified src/HOL/Factorial.thy (diff)
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy (diff)
The file was modified src/HOL/Library/Numeral_Type.thy (diff)
The file was modified src/HOL/Library/Uprod.thy (diff)
The file was modified src/HOL/Set_Interval.thy (diff)