# HG changeset patch
# User wenzelm
# Date 1535651976 -7200
# Node ID 9207ada0ca3164bb0a8257d7a7b4719598a837db
# Parent  8825efd1c2cff1ad6cbda51a2ed4c000bb546be4# Parent  e1796b8ddbae534055428c4fe898654a5ead6498
merged

diff -r e1796b8ddbae -r 9207ada0ca31 NEWS
--- 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 ***
 
diff -r e1796b8ddbae -r 9207ada0ca31 src/HOL/Tools/ATP/scripts/remote_atp
--- 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 = (