# HG changeset patch
# User blanchet
# Date 1435309713 -7200
# Node ID 6ac3172985d4494e3bd3106315e806526224b9da
# Parent  a645a0e6d790379ab78aead96fbd13d1885c619a
updated SystemOnTPTP URL

diff -r a645a0e6d790 -r 6ac3172985d4 NEWS
--- a/NEWS	Fri Jun 26 00:14:10 2015 +0200
+++ b/NEWS	Fri Jun 26 11:08:33 2015 +0200
@@ -126,6 +126,7 @@
   - 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 a645a0e6d790 -r 6ac3172985d4 src/HOL/Tools/ATP/scripts/remote_atp
--- a/src/HOL/Tools/ATP/scripts/remote_atp	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Tools/ATP/scripts/remote_atp	Fri Jun 26 11:08:33 2015 +0200
@@ -12,7 +12,7 @@
 use LWP;
 
 my $SystemOnTPTPFormReplyURL =
-  "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
+  "http://pages.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
 
 # default parameters
 my %URLParameters = (