Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. obsolete (see f3378101f555);
  2. merged
  3. more direct unlimited smt_timeout; update of certificates: generated command-line options are part of input / digest;
  4. clarified smt: support Timeout.ignored and Timeout.scale_time;
  5. clarified timeouts in Isabelle/ML;
  6. tuned --- more elementary Time operations;
  7. removed unused/pointless operation: Time.start is the load/init time of this Scala module;
  8. obsolete;
  9. clarified signature --- augment existing structure Time;
  10. rebuild SMT certificates from scratch;
  11. added lemmas (sublist|prefix|suffix)_list_all
  12. added lemmas takeWhile_is_prefix, suffix_dropWhile, and sublist_(take|drop)While
  13. added lemmas list_all_(take|drop)I and list_all_(take|drop)WhileI
  14. typo
  15. merged
  16. added upper bound on monomorphisation duplicate instances
  17. tuned best_slices in atp_config
  18. tuned exec field in atp_config
Changeset 73391:f16f209f996c by wenzelm:
obsolete (see f3378101f555);
The file was modified src/HOL/SMT_Examples/SMT_Examples_Verit.thy (diff)
Changeset 73390:3c5a7746ffa4 by wenzelm:
merged
Changeset 73389:f3378101f555 by wenzelm:
more direct unlimited smt_timeout;<br>update of certificates: generated command-line options are part of input / digest;
The file was modified src/HOL/SMT.thy (diff)
The file was modified src/HOL/SMT_Examples/Boogie_Dijkstra.certs (diff)
The file was modified src/HOL/SMT_Examples/Boogie_Max.certs (diff)
The file was modified src/HOL/SMT_Examples/SMT_Examples.certs (diff)
The file was modified src/HOL/SMT_Examples/SMT_Word_Examples.certs (diff)
The file was modified src/HOL/SMT_Examples/VCC_Max.certs (diff)
The file was modified src/HOL/Tools/SMT/smt_config.ML (diff)
Changeset 73388:a40e69fde2b4 by wenzelm:
clarified smt: support Timeout.ignored and Timeout.scale_time;
The file was modified src/HOL/Tools/SMT/smt_config.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_systems.ML (diff)
The file was modified src/Pure/Concurrent/timeout.ML (diff)
Changeset 73387:3b5196dac4c8 by wenzelm:
clarified timeouts in Isabelle/ML;
The file was modified NEWS (diff)
The file was modified etc/options (diff)
The file was modified src/HOL/Library/refute.ML (diff)
The file was modified src/HOL/Nitpick_Examples/minipick.ML (diff)
The file was modified src/HOL/Tools/Nitpick/nitpick.ML (diff)
The file was modified src/HOL/Tools/Nitpick/nitpick_tests.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML (diff)
The file was modified src/Pure/Concurrent/timeout.ML (diff)
Changeset 73386:3fb201ca8fb5 by wenzelm:
tuned --- more elementary Time operations;
The file was modified src/HOL/Tools/Nitpick/nitpick.ML (diff)
The file was modified src/HOL/Tools/Nunchaku/nunchaku.ML (diff)
The file was modified src/HOL/Tools/try0.ML (diff)
Changeset 73385:1892708fd148 by wenzelm:
removed unused/pointless operation: Time.start is the load/init time of this Scala module;
The file was modified src/Pure/General/time.scala (diff)
Changeset 73384:d21dbfd3d69b by wenzelm:
obsolete;
The file was modified src/Pure/ML/ml_init.ML (diff)
The file was modified src/Pure/ML/ml_statistics.ML (diff)
Changeset 73383:6b104dc069de by wenzelm:
clarified signature --- augment existing structure Time;
The file was addedsrc/Pure/General/time.ML
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_util.ML (diff)
The file was modified src/Pure/ROOT.ML (diff)
Changeset 73382:2b1b7b58d0e7 by wenzelm:
rebuild SMT certificates from scratch;
The file was modified src/HOL/SMT_Examples/Boogie_Dijkstra.certs (diff)
The file was modified src/HOL/SMT_Examples/Boogie_Max.certs (diff)
The file was modified src/HOL/SMT_Examples/SMT_Examples.certs (diff)
The file was modified src/HOL/SMT_Examples/SMT_Examples_Verit.certs (diff)
The file was modified src/HOL/SMT_Examples/SMT_Word_Examples.certs (diff)
The file was modified src/HOL/SMT_Examples/VCC_Max.certs (diff)
Changeset 73381:3fdb94d87e0e by desharna:
added lemmas (sublist|prefix|suffix)_list_all
The file was modified src/HOL/Library/Sublist.thy (diff)
Changeset 73380:99c1c4f89605 by desharna:
added lemmas takeWhile_is_prefix, suffix_dropWhile, and sublist_(take|drop)While
The file was modified src/HOL/Library/Sublist.thy (diff)
Changeset 73379:b867b436f372 by desharna:
added lemmas list_all_(take|drop)I and list_all_(take|drop)WhileI
The file was modified src/HOL/List.thy (diff)
Changeset 73378:10f5f5b880f4 by haftmann:
typo
The file was modified NEWS (diff)
Changeset 73377:39826af584bf by desharna:
merged
Changeset 73376:96ef620c8b1e by desharna:
added upper bound on monomorphisation duplicate instances
The file was modified src/HOL/Tools/monomorph.ML (diff)
Changeset 73375:a80fd78c85bd by desharna:
tuned best_slices in atp_config
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML (diff)
Changeset 73374:316e12147698 by desharna:
tuned exec field in atp_config
The file was modified src/HOL/TPTP/atp_theory_export.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML (diff)