Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. clarified File_Format.detect: needs to operate on full node name;
  2. more accurate syntax, following Sessions.parse_roots in Scala;
  3. PIDE support for session ROOTS;
  4. more robust;
  5. more Unicode;
  6. eliminated odd "Read_me";
  7. eliminated odd "Read_me";
  8. tuned signature;
  9. silently ignore markup that starts out as singularity, e.g. <language/> from empty ML file;
  10. moved some lemmas from AFP to distribution
Changeset 72839:a597300290de by wenzelm:
clarified File_Format.detect: needs to operate on full node name;
The file was modified src/Pure/Thy/file_format.scala (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 72838:27a7a5499511 by wenzelm:
more accurate syntax, following Sessions.parse_roots in Scala;
The file was modified src/Pure/Pure.thy (diff)
Changeset 72837:2c26c283f3ee by wenzelm:
PIDE support for session ROOTS;
The file was modified NEWS (diff)
The file was modified etc/settings (diff)
The file was modified src/Pure/Pure.thy (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 72836:ec61e1767689 by wenzelm:
more robust;
The file was modified src/Pure/Thy/bibtex.scala (diff)
Changeset 72835:66ca5016b008 by wenzelm:
more Unicode;
The file was modified src/HOL/HOLCF/IMP/HoareEx.thy (diff)
The file was modified src/HOL/HOLCF/IOA/ABP/Check.ML (diff)
The file was modified src/HOL/HOLCF/Lift.thy (diff)
The file was modified src/HOL/ROOT (diff)
Changeset 72834:a025f845fd41 by wenzelm:
eliminated odd &quot;Read_me&quot;;
The file was addedsrc/HOL/HOLCF/IOA/NTP/Overview.thy
The file was modified src/HOL/ROOT (diff)
The file was removedsrc/HOL/HOLCF/IOA/NTP/Read_me
Changeset 72833:fe7df3f7412e by wenzelm:
eliminated odd &quot;Read_me&quot;;
The file was modified src/HOL/ROOT (diff)
The file was removedsrc/HOL/HOLCF/IOA/ABP/Read_me
Changeset 72832:03803bbfdca3 by wenzelm:
tuned signature;
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/mkroot.scala (diff)
Changeset 72831:ffae996e9c08 by wenzelm:
silently ignore markup that starts out as singularity, e.g. &lt;language/&gt; from empty ML file;
The file was modified src/Pure/PIDE/command.scala (diff)
Changeset 72830:ec0d3a62bb3b by haftmann:
moved some lemmas from AFP to distribution
The file was modified src/HOL/Library/Bit_Operations.thy (diff)
The file was modified src/HOL/Library/Word.thy (diff)
The file was modified src/HOL/Power.thy (diff)