# HG changeset patch
# User blanchet
# Date 1280351135 -7200
# Node ID a7c9cc973ca1bfe20ae23b039a3fd2acdaf7f9f3
# Parent  685d1f0f75b37ba047c1010c61d33f2b4fc058bf
fiddled with usage text

diff -r 685d1f0f75b3 -r a7c9cc973ca1 src/HOL/Tools/ATP/scripts/remote_atp
--- a/src/HOL/Tools/ATP/scripts/remote_atp	Wed Jul 28 23:01:27 2010 +0200
+++ b/src/HOL/Tools/ATP/scripts/remote_atp	Wed Jul 28 23:05:35 2010 +0200
@@ -2,6 +2,7 @@
 #
 # Wrapper for custom remote provers on SystemOnTPTP
 # Author: Fabian Immler, TU Muenchen
+# Author: Jasmin Blanchette, TU Muenchen
 #
 
 use warnings;
@@ -28,14 +29,14 @@
 
 #----Usage
 sub usage() {
-  print("Usage: remote_atp [<options>] <File name>\n");
-  print("    <options> are ...\n");
-  print("    -h            - print this help\n");
-  print("    -w            - list available ATP systems\n");
-  print("    -s<system>    - specified system to use\n");
-  print("    -t<timelimit> - CPU time limit for system\n");
-  print("    -c<command>   - custom command for system\n");
-  print("    <File name>   - TPTP problem file\n");
+  print("Usage: remote_atp [<options>] <file_name>\n");
+  print("Options:\n");
+  print("    -h              print this help\n");
+  print("    -w              list available ATPs\n");
+  print("    -s<system>      ATP to use\n");
+  print("    -t<time_limit>  CPU time limit for ATP\n");
+  print("    -c<command>     custom ATP invocation command\n");
+  print("    <file_name>     TPTP problem file\n");
   exit(0);
 }
 if (exists($Options{'h'})) {