# HG changeset patch
# User blanchet
# Date 1535647253 -7200
# Node ID 8825efd1c2cff1ad6cbda51a2ed4c000bb546be4
# Parent  511d163ab623b0d419e2ed2bd22a5cf94fd5f9da
updated URL to remote TPTP, following heads-up from Geoff Sutcliffe

diff -r 511d163ab623 -r 8825efd1c2cf NEWS
--- a/NEWS	Wed Aug 29 20:01:39 2018 +0200
+++ b/NEWS	Thu Aug 30 18:40:53 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 511d163ab623 -r 8825efd1c2cf src/HOL/Tools/ATP/scripts/remote_atp
--- a/src/HOL/Tools/ATP/scripts/remote_atp	Wed Aug 29 20:01:39 2018 +0200
+++ b/src/HOL/Tools/ATP/scripts/remote_atp	Thu Aug 30 18:40:53 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 = (