# HG changeset patch
# User desharna
# Date 1639911054 -3600
# Node ID a7183a0a33e1fb7f4f4699f68cf20c6a090f2117
# Parent  6f5eafd952c964abd34d8019757992d57549c425
NEWS

diff -r 6f5eafd952c9 -r a7183a0a33e1 NEWS
--- a/NEWS	Sun Dec 19 11:15:21 2021 +0100
+++ b/NEWS	Sun Dec 19 11:50:54 2021 +0100
@@ -34,6 +34,16 @@
   - Lifted multiple lemmas from mult to multp.
   - Redefined less_multiset to be based on multp. INCOMPATIBILITY.
 
+* Sledgehammer:
+  - Introduced sledgehammer_outcome data type and changed return type of ML
+    function Sledgehammer.run_sledgehammer from "bool * (string * string list)"
+    to "bool * (sledgehammer_outcome * string)". The former value can be
+    recomputed with "apsnd (ATP_Util.map_prod
+    Sledgehammer.short_string_of_sledgehammer_outcome single)".
+    INCOMPATIBILITY.
+  - Added support for TX0 and TX1 TPTP formats and $ite/$let expressions
+    in TH0 and TH1.
+
 
 New in Isabelle2021-1 (December 2021)
 -------------------------------------