merged
authorwenzelm
Thu, 30 Aug 2018 19:59:36 +0200
changeset 68859 9207ada0ca31
parent 68848 8825efd1c2cf (diff)
parent 68858 e1796b8ddbae (current diff)
child 68860 f443ec10447d
child 68861 2d99562a7fe2
merged
--- 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 = (