--- a/NEWS Tue Aug 03 13:53:22 2021 +0000
+++ b/NEWS Wed Aug 04 08:27:16 2021 +0200
@@ -201,7 +201,7 @@
INCOMPATIBILITY.
* Sledgehammer:
- - Removed legacy "lam_lifting" (synonym for "liftinng") from option
+ - Removed legacy "lam_lifting" (synonym for "lifting") from option
"lam_trans". Minor INCOMPATIBILITY.
- Renamed "hide_lams" to "opaque_lifting" in option "lam_trans".
Minor INCOMPATIBILITY.
--- a/src/HOL/Tools/ATP/atp_proof.ML Tue Aug 03 13:53:22 2021 +0000
+++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Aug 04 08:27:16 2021 +0200
@@ -55,6 +55,7 @@
val zipperpositionN : string
val remote_prefix : string
val dummy_tfxN : string
+ val dummy_thfN : string
val agsyhol_core_rule : string
val spass_input_rule : string
@@ -117,6 +118,7 @@
val zipperpositionN = "zipperposition"
val remote_prefix = "remote_"
val dummy_tfxN = "dummy_tfx"
+val dummy_thfN = "dummy_thf"
val agsyhol_core_rule = "__agsyhol_core" (* arbitrary *)
val spass_input_rule = "Inp"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Tue Aug 03 13:53:22 2021 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed Aug 04 08:27:16 2021 +0200
@@ -682,10 +682,13 @@
best_max_new_mono_instances = default_max_new_mono_instances}
val dummy_tfx_format = TFF (With_FOOL, Polymorphic)
-
val dummy_tfx_config = dummy_config Hypothesis dummy_tfx_format "mono_native_fool" false
val dummy_tfx = (dummy_tfxN, fn () => dummy_tfx_config)
+val dummy_thf_format = THF (With_FOOL, Polymorphic, THF_With_Choice)
+val dummy_thf_config = dummy_config Hypothesis dummy_thf_format "mono_native_higher_fool" false
+val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
+
(* Setup *)
@@ -722,7 +725,7 @@
val atps =
[agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition,
remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3,
- remote_waldmeister, remote_zipperposition, dummy_tfx]
+ remote_waldmeister, remote_zipperposition, dummy_tfx, dummy_thf]
val _ = Theory.setup (fold add_atp atps)