rewording and reordering some of the command line argument descriptsion

doc/Reference.md

@@ -1009,7 +1009,7 @@ See the entry for [Biconditional](#biconditional-if-and-only-if).
 A formula `if P then Q` is true when both `P` and `Q` are true and it
 is true when `P` is false.
 
-To prove a conditional formula, use `assume`. (See the entry for Assume.)
+To prove a conditional formula, use `assume`. (See the entry for [Assume](#assume).)
 
 To use a given that is a conditional formula, use `apply`-`to`.
 (See the entry for [Apply-To](#apply-to-proof-modus-ponens).)

index.md

@@ -123,43 +123,65 @@ next in a proof.
 
 ## Command Line Arguments
 
-The `deduce.py` script supports certain command line arguments which are documented below. If an argument isn't recognized, then it is automatically treated as a directory/file to be interpreted by Deduce.
+The `deduce.py` script supports certain command line arguments which
+are documented below. If an argument is not preceeded by one of the
+keywords listed below, then it is treated as the name of a file or
+directory and will be processed by Deduce.
 
-`--dir library-directory`
+`--dir directory-name`
 
-Tells Deduce to link `library-directory` when interpreting a file. For example, if `test.pf` imports `Church.pf`, and `Church.pf` resides in a folder named `libraries`, then `--dir libraries` will allow `test.pf` to import `Church.pf`. Note that `--dir` expects a directory, not an individual file.
-
-`--error`
-
-Deduce will now expect all files that it interprets to contain an error, and will exit gracefully if the file contains an error. However if no error is caught, it will exit with a return code of 255.
+Tells Deduce to include the given `directory-name` in the list of
+directories to search when importing a file. For example, if `test.pf`
+imports `Curry`, and `Curry.pf` resides in a folder named `howard`,
+then `--dir howard` will allow `test.pf` to import `Church`. Note that
+`--dir` expects a directory name, not an individual file.
 
 `--no-stdlib`
 
-Deduce, by default, will locate and link the standard library (in `/lib` of the Deduce repository). However if this argument is supplied, it won't do so.
+Deduce, by default, will locate and link the standard library (in
+`/lib` of the Deduce repository). However if this argument is
+supplied, it will not do so.
 
 `--lalr`
 
-Deduce normally uses a custom recursive descent parser to parse any input files, however this argument will make Deduce instead use lark's LALR parser. This argument exists solely for checking that `Deduce.lark` maintains parity with the recursive descent parser.
+Deduce normally uses a custom recursive descent parser to parse any
+input files, however this argument will make Deduce instead use lark's
+LALR parser. This argument exists solely for checking that
+`Deduce.lark` maintains parity with the recursive descent parser.
 
 `--recursive-descent`
 
-Tells Deduce to use the recursive descent (default) parser. If `--lalr` is also supplied, then only the recursive descent parser will be used.
+Tells Deduce to use the recursive descent (default) parser. If
+`--lalr` is also supplied, then only the recursive descent parser will
+be used.
 
 `--recursive-directories` or `-r`
 
-Instead of only interpreter files in a top level directory, Deduce will now descend into any subdirectories.
+Instead of only processing files in the specified directories, Deduce
+will also descend into any subdirectories.
 
 `--traceback`
 
-Prints out an exception if an interpreted file throws one.
+Prints out the exception if processing a file triggers an error.
 
 `--unique-names`
 
-Prints out all variables and types with an unique name. For example, if a program defines an overloaded function `fun`, `fun` might instead be printed out as `fun.1` everytime one overload appears but everytime another overload is referenced it would be printed out as `fun.2` instead.
+Prints out all variables and types with an unique name. For example,
+if a program defines a variable `x` in several different scopes, `x`
+would instead be printed out as `x.1` in one scope and printed as
+`x.2` in a different scope.
 
 `--verbose`
 
-Makes Deduce print out ALL debug logs. It is generally recommended to use `--traceback` instead, as this argument can make Deduce print out hundreds of thousands of lines.
+Makes Deduce print out the debug logs. It is generally recommended to
+use `--traceback` instead, as this argument can make Deduce print out
+thousands of lines.
+
+`--error`
+
+Deduce will expect all files that it processes to contain an error. If
+there is a file that does not contain an error, Deduce will exit with
+a return code of 255.
 
 
 ## Syntax/Grammar Overview