Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. position information for literal facts; Markup.entry may have empty kind/name;
  3. tuned;
  4. tuned;
Changeset 63338:94c6e3ed0afb by wenzelm:
merged
Changeset 63337:ae9330fdbc16 by wenzelm:
position information for literal facts;<br>Markup.entry may have empty kind/name;
The file was modified src/HOL/Mirabelle/Tools/mirabelle_metis.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML (diff)
The file was modified src/Pure/Isar/proof_context.ML (diff)
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/facts.ML (diff)
The file was modified src/Tools/jEdit/src/rendering.scala (diff)
Changeset 63336:054a92af0f2b by wenzelm:
tuned;
The file was modified src/Pure/Isar/attrib.ML (diff)
Changeset 63335:d98164344ec1 by wenzelm:
tuned;
The file was modified src/Pure/General/binding.ML (diff)