Skip to content
Failed

Changes

Summary

  1. some updates and clarification on Assumption.export_term;
  2. new theorem has_integral_UN
  3. updated to jdk-17.0.2+8;
  4. used elapsed time instead of cpu time in Mirabelle because the latter contain cpu time of all threads
  5. NEWS
  6. added Mirabelle option "-y" for dry run
  7. tuned garbage optimization
  8. added cpu time (in ms) to Mirabelle run_action output
  9. added Mirabelle option -r to randomize the goals before selection
  10. A new lemma about inverse image
  11. proper treatment of $let variables in symbol table in Sledgehammer
  12. removed unconditional TPTP symbol declaration for undefined_bool in sledgehammer
Changeset 74994:26794ec7c78e by wenzelm:
some updates and clarification on Assumption.export_term;
The file was modified src/Doc/Implementation/Proof.thy
Changeset 74993:e9a514c70b9a by paulson _lp15@cam.ac.uk_:
new theorem has_integral_UN
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
Changeset 74992:79635df97a90 by wenzelm:
updated to jdk-17.0.2+8;
The file was modified Admin/components/components.sha1
The file was modified Admin/components/main
Changeset 74991:d699eb2d26ad by desharna:
used elapsed time instead of cpu time in Mirabelle because the latter contain cpu time of all threads
The file was modified src/HOL/Tools/Mirabelle/mirabelle.ML
Changeset 74990:7c123c76a8c9 by desharna:
NEWS
The file was modified NEWS
Changeset 74989:003f378b78a5 by desharna:
added Mirabelle option "-y" for dry run
The file was modified src/HOL/Tools/Mirabelle/mirabelle.ML
The file was modified src/HOL/Tools/Mirabelle/mirabelle.scala
The file was modified src/HOL/Tools/etc/options
Changeset 74988:9fcf09cf7b36 by desharna:
tuned garbage optimization
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML
Changeset 74987:877f0c44d77e by desharna:
added cpu time (in ms) to Mirabelle run_action output
The file was modified src/HOL/Tools/Mirabelle/mirabelle.ML
The file was modified src/HOL/Tools/Mirabelle/mirabelle.scala
Changeset 74986:fc664e4fbf6d by desharna:
added Mirabelle option -r to randomize the goals before selection
The file was addedsrc/HOL/Tools/Mirabelle/mirabelle_util.ML
The file was modified src/HOL/Mirabelle.thy
The file was modified src/HOL/Tools/Mirabelle/mirabelle.ML
The file was modified src/HOL/Tools/Mirabelle/mirabelle.scala
The file was modified src/HOL/Tools/etc/options
Changeset 74985:ac3901e4e0a9 by paulson _lp15@cam.ac.uk_:
A new lemma about inverse image
The file was modified src/HOL/Finite_Set.thy
Changeset 74984:192876ea202d by desharna:
proper treatment of $let variables in symbol table in Sledgehammer
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML
Changeset 74983:b87fcf474e7f by desharna:
removed unconditional TPTP symbol declaration for undefined_bool in sledgehammer
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML

Summary

  1. Removal of a lemma (now in the libraries) and a few tweaks
Changeset 12362:81aae6b30ce5 by paulson _lp15@cam.ac.uk_:
Removal of a lemma (now in the libraries) and a few tweaks
The file was modified thys/Szemeredi_Regularity/Szemeredi.thy