Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more operations;
  2. merged
  3. return exports as result for Isabelle server;
  4. more checks;
  5. tuned;
  6. more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure; tuned;
  7. clarified signature; avoid pointless compression;
  8. store exports within PIDE command state; Markup.Export.unapply: proper NAME;
  9. removed some lemma duplicates
  10. typo
  11. more appropriate notion of emptiness
  12. merged
  13. more tidying
  14. starting to tidy up Interval_Integral.thy
Changeset 68108:2277fe496d78 by wenzelm:
more operations;
The file was modified src/Pure/General/bytes.scala (diff)
Changeset 68107:3687109009c4 by wenzelm:
merged
Changeset 68106:a514e29db980 by wenzelm:
return exports as result for Isabelle server;
The file was modified src/Doc/System/Server.thy (diff)
The file was modified src/Pure/General/bytes.scala (diff)
The file was modified src/Pure/Thy/thy_resources.scala (diff)
The file was modified src/Pure/Tools/server_commands.scala (diff)
Changeset 68105:577072a0ceed by wenzelm:
more checks;
The file was modified src/Pure/Thy/export.ML (diff)
Changeset 68104:3795f67716e6 by wenzelm:
tuned;
The file was modified src/Pure/Thy/export.scala (diff)
Changeset 68103:c5764b8b2a87 by wenzelm:
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;<br>tuned;
The file was modified src/Pure/PIDE/session.scala (diff)
The file was modified src/Pure/Thy/export.scala (diff)
Changeset 68102:813b5d0904c6 by wenzelm:
clarified signature;<br>avoid pointless compression;
The file was modified src/Pure/Thy/export.ML (diff)
The file was modified src/Pure/Thy/export.scala (diff)
Changeset 68101:0699a0bacc50 by wenzelm:
store exports within PIDE command state;<br>Markup.Export.unapply: proper NAME;
The file was modified src/Pure/PIDE/command.scala (diff)
The file was modified src/Pure/PIDE/document.scala (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/PIDE/session.scala (diff)
The file was modified src/Pure/Thy/export.ML (diff)
The file was modified src/Pure/Thy/export.scala (diff)
Changeset 68100:b2d84b1114fa by haftmann:
removed some lemma duplicates
The file was modified NEWS (diff)
The file was modified src/HOL/Divides.thy (diff)
The file was modified src/HOL/Groebner_Basis.thy (diff)
The file was modified src/HOL/Presburger.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)
Changeset 68099:305f9f3edf05 by haftmann:
typo
The file was modified src/HOL/Tools/string_syntax.ML (diff)
Changeset 68098:e2bb1d95cbd0 by haftmann:
more appropriate notion of emptiness
The file was modified src/Pure/Isar/class.ML (diff)
Changeset 68097:5f3cffe16311 by paulson:
merged
Changeset 68096:e58c9ac761cb by paulson _lp15@cam.ac.uk_:
more tidying
The file was modified src/HOL/Analysis/Interval_Integral.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
Changeset 68095:4fa3e63ecc7e by paulson _lp15@cam.ac.uk_:
starting to tidy up Interval_Integral.thy
The file was modified src/HOL/Analysis/Derivative.thy (diff)
The file was modified src/HOL/Analysis/Interval_Integral.thy (diff)
The file was modified src/HOL/Library/Extended_Real.thy (diff)