--- a/NEWS Thu Aug 30 19:52:30 2018 +0200
+++ b/NEWS Thu Aug 30 19:59:36 2018 +0200
@@ -22,6 +22,9 @@
SUPREMUM, UNION, INTER should now rarely occur in output and are just
retained as migration auxiliary. INCOMPATIBILITY.
+* Sledgehammer: The URL for SystemOnTPTP, which is used by remote
+provers, has been updated.
+
*** ML ***
--- a/src/HOL/Tools/ATP/scripts/remote_atp Thu Aug 30 19:52:30 2018 +0200
+++ b/src/HOL/Tools/ATP/scripts/remote_atp Thu Aug 30 19:59:36 2018 +0200
@@ -12,7 +12,7 @@
use LWP;
my $SystemOnTPTPFormReplyURL =
- "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
+ "http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply";
# default parameters
my %URLParameters = (