--- a/NEWS Mon Jul 06 10:47:30 2020 +0000
+++ b/NEWS Mon Jul 06 16:52:48 2020 +0200
@@ -81,6 +81,10 @@
into theories Misc_lsb, Misc_msb and Misc_set_bit respectively.
INCOMPATIBILITY.
+* Session HOL-TPTP: The "tptp_isabelle" and "tptp_sledgehammer"
+commands are in working order again, as opposed to outputting
+"GaveUp" on nearly all problems.
+
* Simproc defined_all and rewrite rule subst_all perform
more aggressive substitution with variables from assumptions.
INCOMPATIBILITY, use something like