Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. proper name (amending 742d94015918);
  2. invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process);
  3. avoid odd PIDE markup, notably in kokodi input;
  4. clarified names;
  5. clarified signature;
  6. clarified signature;
  7. proper treatment of timeout: <= 0 means already timed out, but for $KODKODI/bin/kodkodi it would mean NO timeout;
  8. proper treatment of absolute deadline vs. relative timeout;
  9. clarified session: no parent image for minor theory imports;
  10. removed obsolete created_temp_dir: ISABELLE_TMP is always present for the running Isabelle/ML process;
  11. more lemmas
  12. proper syntax declaration
Changeset 72197:957bf00eff2a by wenzelm:
proper name (amending 742d94015918);
The file was modified src/Doc/System/Scala.thy (diff)
Changeset 72196:6dba090358d2 by wenzelm:
invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process);
The file was addedsrc/HOL/Tools/etc/settings
The file was modified src/HOL/Tools/Nitpick/kodkod.ML (diff)
The file was modified src/HOL/Tools/Nitpick/kodkod.scala (diff)
The file was modified src/HOL/Tools/etc/options (diff)
Changeset 72195:16f2288b30cf by wenzelm:
avoid odd PIDE markup, notably in kokodi input;
The file was modified src/HOL/Tools/Nitpick/nitpick.ML (diff)
The file was modified src/HOL/Tools/Nitpick/nitpick_scope.ML (diff)
Changeset 72194:eef421b724c0 by wenzelm:
clarified names;
The file was modified src/Pure/System/scala.scala (diff)
The file was modified src/Pure/Thy/bibtex.ML (diff)
The file was modified src/Pure/Thy/bibtex.scala (diff)
Changeset 72193:742d94015918 by wenzelm:
clarified signature;
The file was modified etc/settings (diff)
The file was modified src/Pure/System/scala.scala (diff)
The file was modified src/Pure/Thy/bibtex.scala (diff)
Changeset 72192:07635a1b6fd2 by wenzelm:
clarified signature;
The file was modified src/Pure/Concurrent/isabelle_thread.scala (diff)
Changeset 72191:d436ba9ac9aa by wenzelm:
proper treatment of timeout: &lt;= 0 means already timed out, but for $KODKODI/bin/kodkodi it would mean NO timeout;
The file was modified src/HOL/Tools/Nitpick/kodkod.ML (diff)
Changeset 72190:8009c4b5db5e by wenzelm:
proper treatment of absolute deadline vs. relative timeout;
The file was modified src/HOL/Nitpick_Examples/minipick.ML (diff)
The file was modified src/HOL/Tools/Nitpick/nitpick_tests.ML (diff)
Changeset 72189:7a213affdc10 by wenzelm:
clarified session: no parent image for minor theory imports;
The file was modified src/HOL/ROOT (diff)
Changeset 72188:b155681b9f6a by wenzelm:
removed obsolete created_temp_dir: ISABELLE_TMP is always present for the running Isabelle/ML process;
The file was modified src/HOL/Tools/Nitpick/kodkod.ML (diff)
Changeset 72187:e4aecb0c7296 by haftmann:
more lemmas
The file was modified src/HOL/Divides.thy (diff)
The file was modified src/HOL/Euclidean_Division.thy (diff)
The file was modified src/HOL/Groups_List.thy (diff)
The file was modified src/HOL/Library/Bit_Operations.thy (diff)
The file was modified src/HOL/Parity.thy (diff)
Changeset 72186:bdf77466b6c8 by haftmann:
proper syntax declaration
The file was modified src/HOL/Statespace/state_space.ML (diff)