Changes

Summary

merged
optimized facts traversal in TPTP translation
optimized app_op_level selection in TPTP generation
tuned trivial check in mirabelle_sledgehammer
renamed run_action to run in Mirabelle.action record
added spying of fact filtering timing
tuned mirabelle_sledgehammer output
added spying to Sledgehammer
proper fact filter for dummy ATPs
added syping of fact filtering time to sledgehammer
removed unsynchronized references in mirabelle_sledgehammer
tuned mirabelle_sledgehammer to have a single call to Synchronized.change per run

Changeset 75007:2e16798b6f2b by desharna: merged
Changeset 75006:01bb90de56bb by desharna: optimized facts traversal in TPTP translation
The file was modified	`src/HOL/Tools/ATP/atp_problem_generate.ML` (diff)
Changeset 75005:4106bc2a9cc8 by desharna: optimized app_op_level selection in TPTP generation
The file was modified	`src/HOL/Tools/ATP/atp_problem_generate.ML` (diff)
The file was modified	`src/HOL/Tools/ATP/atp_util.ML` (diff)
Changeset 75004:8dc52ba4155b by desharna: tuned trivial check in mirabelle_sledgehammer
The file was modified	`src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML` (diff)
Changeset 75003:f21e7e6172a0 by desharna: renamed run_action to run in Mirabelle.action record
The file was modified	`NEWS` (diff)
The file was modified	`src/HOL/Tools/Mirabelle/mirabelle.ML` (diff)
The file was modified	`src/HOL/Tools/Mirabelle/mirabelle_arith.ML` (diff)
The file was modified	`src/HOL/Tools/Mirabelle/mirabelle_metis.ML` (diff)
The file was modified	`src/HOL/Tools/Mirabelle/mirabelle_presburger.ML` (diff)
The file was modified	`src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML` (diff)
The file was modified	`src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML` (diff)
The file was modified	`src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML` (diff)
The file was modified	`src/HOL/Tools/Mirabelle/mirabelle_try0.ML` (diff)
Changeset 75002:ef18787842b3 by desharna: added spying of fact filtering timing
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer.ML` (diff)
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML` (diff)
Changeset 75001:d9a5824f68c8 by desharna: tuned mirabelle_sledgehammer output
The file was modified	`src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML` (diff)
Changeset 75000:4466fae54ff9 by desharna: added spying to Sledgehammer
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML` (diff)
Changeset 74999:300463f379bf by desharna: proper fact filter for dummy ATPs
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML` (diff)
Changeset 74998:fe14ceff1cfd by desharna: added syping of fact filtering time to sledgehammer
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer.ML` (diff)
Changeset 74997:d4a52993a81e by desharna: removed unsynchronized references in mirabelle_sledgehammer
The file was modified	`src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML` (diff)
Changeset 74996:1f4c39ffb116 by desharna: tuned mirabelle_sledgehammer to have a single call to Synchronized.change per run
The file was modified	`src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML` (diff)