# HG changeset patch
# User blanchet
# Date 1440699040 -7200
# Node ID b09461b3bc057dbf2a5ee18571c137ba4854c0b9
# Parent  99d58362eeeb0eca7f34e85f41962a7c939d299e
reverted 6ac3172985d4 -- the old URL has been restored

diff -r 99d58362eeeb -r b09461b3bc05 NEWS
--- a/NEWS	Thu Aug 27 19:55:43 2015 +0200
+++ b/NEWS	Thu Aug 27 20:10:40 2015 +0200
@@ -192,7 +192,6 @@
   - Proof reconstruction has been improved, to minimize the incidence of
     cases where Sledgehammer gives a proof that does not work.
   - Auto Sledgehammer now minimizes and preplays the results.
-  - The URL for remote provers on SystemOnTPTP has been updated.
 
 * Nitpick:
   - Removed "check_potential" and "check_genuine" options.
diff -r 99d58362eeeb -r b09461b3bc05 src/HOL/Tools/ATP/scripts/remote_atp
--- a/src/HOL/Tools/ATP/scripts/remote_atp	Thu Aug 27 19:55:43 2015 +0200
+++ b/src/HOL/Tools/ATP/scripts/remote_atp	Thu Aug 27 20:10:40 2015 +0200
@@ -12,7 +12,7 @@
 use LWP;
 
 my $SystemOnTPTPFormReplyURL =
-  "http://pages.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
+  "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
 
 # default parameters
 my %URLParameters = (