diff --git a/set.mm b/set.mm
index 6b7058464..77ad546dd 100644
--- a/set.mm
+++ b/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.
- Statements with hypotheses. 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 `
- & ` |- ( ph -> ps ) ` => ` |- ps ` ". These symbols are _not_
- part of the Metamath language but are just informal notation meaning
- "and" and "implies".
+ Statements with hypotheses.
+ 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".
Discouraged use and modification.