Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more formal contributors (with the help of the history);
  2. proper data columns for plots;
  3. merged
  4. tuned -- Toplevel.presentation_context is total;
  5. document markers are formal comments, and may thus occur anywhere in the command-span; clarified Outer_Syntax.parse_span, Outer_Syntax.parse_text wrt. span structure; tuned signature;
  6. PIDE markup for spell-checking;
  7. markup and document markers for some meta data from "Dublin Core Metadata Element Set";
  8. tuned;
  9. added semantic document markers; emulate old-style tags as "tag" markers, with subtle change of semantics for multiples tags (ever used?); tuned;
  10. clarified signature;
  11. added glyph for \<marker>;
  12. tuned proof;
  13. clarified Toplevel.state: more explicit types; presentation context is always present, with default to Pure.thy and fall-back to Pure bootstrap theory;
  14. tuned;
  15. merged
  16. tidied up HOL/ex/Primrec
Changeset 69895:6b03a8cf092d by wenzelm:
more formal contributors (with the help of the history);
The file was modified src/HOL/Algebra/Congruence.thy (diff)
The file was modified src/HOL/Algebra/Coset.thy (diff)
The file was modified src/HOL/Algebra/Divisibility.thy (diff)
The file was modified src/HOL/Algebra/FiniteProduct.thy (diff)
The file was modified src/HOL/Algebra/Group.thy (diff)
The file was modified src/HOL/Algebra/Ideal.thy (diff)
The file was modified src/HOL/Algebra/Multiplicative_Group.thy (diff)
The file was modified src/HOL/Algebra/Ring.thy (diff)
The file was modified src/HOL/Algebra/RingHom.thy (diff)
The file was modified src/HOL/Library/Multiset.thy (diff)
The file was modified src/HOL/Library/Permutations.thy (diff)
The file was modified src/HOL/Library/Product_Order.thy (diff)
Changeset 69894:2eade8651b93 by wenzelm:
proper data columns for plots;
The file was modified src/Pure/Admin/build_status.scala (diff)
Changeset 69893:1a7857abb75c by wenzelm:
merged
Changeset 69892:f752f3993db8 by wenzelm:
tuned -- Toplevel.presentation_context is total;
The file was modified src/Pure/PIDE/command.ML (diff)
The file was modified src/Pure/Thy/thy_output.ML (diff)
The file was modified src/Pure/Tools/debugger.ML (diff)
Changeset 69891:def3ec9cdb7e by wenzelm:
document markers are formal comments, and may thus occur anywhere in the command-span;<br>clarified Outer_Syntax.parse_span, Outer_Syntax.parse_text wrt. span structure;<br>tuned signature;
The file was modified etc/symbols (diff)
The file was modified src/Pure/General/antiquote.ML (diff)
The file was modified src/Pure/General/comment.ML (diff)
The file was modified src/Pure/General/comment.scala (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/Isar/outer_syntax.ML (diff)
The file was modified src/Pure/Isar/parse.ML (diff)
The file was modified src/Pure/Isar/parse.scala (diff)
The file was modified src/Pure/Isar/token.ML (diff)
The file was modified src/Pure/Isar/token.scala (diff)
The file was modified src/Pure/ML/ml_lex.ML (diff)
The file was modified src/Pure/PIDE/command.ML (diff)
The file was modified src/Pure/PIDE/command.scala (diff)
The file was modified src/Pure/Pure.thy (diff)
The file was modified src/Pure/Syntax/lexicon.ML (diff)
The file was modified src/Pure/Thy/document_marker.ML (diff)
The file was modified src/Pure/Thy/document_source.ML (diff)
The file was modified src/Pure/Thy/thy_header.ML (diff)
The file was modified src/Pure/Thy/thy_info.ML (diff)
The file was modified src/Pure/Thy/thy_output.ML (diff)
The file was modified src/Pure/Tools/rail.ML (diff)
Changeset 69890:cb643a1a5313 by wenzelm:
PIDE markup for spell-checking;
The file was modified src/Pure/Thy/document_marker.ML (diff)
Changeset 69889:be04e9a053a7 by wenzelm:
markup and document markers for some meta data from &quot;Dublin Core Metadata Element Set&quot;;
The file was modified src/Pure/PIDE/markup.ML (diff)
The file was modified src/Pure/PIDE/markup.scala (diff)
The file was modified src/Pure/Thy/document_marker.ML (diff)
Changeset 69888:6db51f45b5f9 by wenzelm:
tuned;
The file was modified src/Pure/Isar/toplevel.ML (diff)
Changeset 69887:b9985133805d by wenzelm:
added semantic document markers;<br>emulate old-style tags as &quot;tag&quot; markers, with subtle change of semantics for multiples tags (ever used?);<br>tuned;
The file was addedsrc/Pure/Thy/document_marker.ML
The file was modified src/Pure/General/symbol.scala (diff)
The file was modified src/Pure/Isar/outer_syntax.ML (diff)
The file was modified src/Pure/Isar/parse.scala (diff)
The file was modified src/Pure/Isar/toplevel.ML (diff)
The file was modified src/Pure/PIDE/command.ML (diff)
The file was modified src/Pure/PIDE/command.scala (diff)
The file was modified src/Pure/PIDE/markup.ML (diff)
The file was modified src/Pure/Pure.thy (diff)
The file was modified src/Pure/ROOT.ML (diff)
The file was modified src/Pure/Thy/document_source.ML (diff)
The file was modified src/Pure/Thy/thy_header.ML (diff)
The file was modified src/Pure/Thy/thy_header.scala (diff)
The file was modified src/Pure/Thy/thy_output.ML (diff)
Changeset 69886:0cb8753bdb50 by wenzelm:
clarified signature;
The file was modified src/Pure/Isar/isar_cmd.ML (diff)
The file was modified src/Pure/Isar/toplevel.ML (diff)
The file was modified src/Pure/PIDE/command.ML (diff)
The file was modified src/Pure/PIDE/document.ML (diff)
The file was modified src/Pure/Thy/thy_info.ML (diff)
The file was modified src/Pure/Thy/thy_output.ML (diff)
The file was modified src/Pure/theory.ML (diff)
Changeset 69885:6dc5506ad449 by wenzelm:
added glyph for \&lt;marker&gt;;
The file was modified Admin/components/components.sha1 (diff)
The file was modified Admin/components/main (diff)
The file was modified etc/symbols (diff)
The file was modified src/Pure/Admin/build_fonts.scala (diff)
Changeset 69884:dec7cc38a5dc by wenzelm:
tuned proof;
The file was modified src/HOL/Computational_Algebra/Euclidean_Algorithm.thy (diff)
Changeset 69883:f8293bf510a0 by wenzelm:
clarified Toplevel.state: more explicit types;<br>presentation context is always present, with default to Pure.thy and fall-back to Pure bootstrap theory;
The file was modified src/Pure/Isar/isar_cmd.ML (diff)
The file was modified src/Pure/Isar/toplevel.ML (diff)
The file was modified src/Pure/PIDE/command.ML (diff)
The file was modified src/Pure/PIDE/document.ML (diff)
The file was modified src/Pure/Thy/thy_info.ML (diff)
The file was modified src/Pure/Thy/thy_output.ML (diff)
Changeset 69882:a9e574e2cba5 by wenzelm:
tuned;
The file was modified src/Pure/Isar/toplevel.ML (diff)
Changeset 69881:6a6cdf34e980 by paulson:
merged
Changeset 69880:fe3c12990893 by paulson _lp15@cam.ac.uk_:
tidied up HOL/ex/Primrec
The file was modified src/HOL/ex/Primrec.thy (diff)