conventions minor edit

set.mm

@@ -422688,7 +422688,7 @@ All axiomatic assertions ($a statements)
        is that we use the
        regular "ax-NAME" label naming convention to define the axiom,
        but we precede it with a proof of the same statement with the label
-       "axNAME" .  An example is complex arithmetic axiom ~ ax-1cn ,
+       "axNAME" .  An example is the complex arithmetic axiom ~ ax-1cn ,
        proven by the preceding theorem ~ ax1cn .
        The Metamath program will warn if an axiom does not match the preceding
        theorem that justifies it if the names match in this way.
@@ -422698,15 +422698,16 @@ All axiomatic assertions ($a statements)
        We encourage definitions to include hypertext links to proven examples.
        </li>
 
-       <li><b>Statements with hypotheses.</b> Many theorems and some axioms,
-       such as ~ ax-mp , have hypotheses that must be satisfied in order for
-       the conclusion to hold, in this case min and maj.  When presented in
-       summarized form such as in the Theorem List (click on "Nearby theorems"
-       on the ~ ax-mp page), the hypotheses are connected with an ampersand and
-       separated from the conclusion with a big arrow, such as in " ` |- ph `
-       &amp; ` |- ( ph -> ps ) ` =&gt; ` |- ps ` ". These symbols are _not_
-       part of the Metamath language but are just informal notation meaning
-       "and" and "implies".
+       <li><b>Statements with hypotheses.</b>
+       Many theorems and some axioms, such as ~ ax-mp , have hypotheses that
+       must be satisfied in order for the conclusion to hold, in this case min
+       and maj.  When displayed in summarized form such as in the "Theorem
+       List" page (to get to it, click on "Nearby theorems" on the ~ ax-mp
+       page), the hypotheses are connected with an ampersand and separated from
+       the conclusion with a double right arrow, such as in
+       " ` |- ph & |- ( ph -> ps ) => |- ps ` ".  These symbols are not part of
+       the Metamath language but are just informal notation meaning "and" and
+       "implies".
        </li>
 
        <li><b>Discouraged use and modification.</b>