corrections

metamath · Nov 17, 2023 · f5de6df · f5de6df
1 parent 3441655
commit f5de6df
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 12 deletions.
diff --git a/tests/min_found.expected b/tests/min_found.expected
@@ -1,6 +1,6 @@
 MM> READ "min_found.mm"
-Reading source file "min_found.mm"... 775 bytes
-775 bytes were read into the source buffer.
+Reading source file "min_found.mm"... 761 bytes
+761 bytes were read into the source buffer.
 The source has 18 statements; 5 are $a and 2 are $p.
 SET EMPTY_SUBSTITUTION was turned ON (allowed) for this database.
 No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *

diff --git a/tests/min_found.mm b/tests/min_found.mm
@@ -1,8 +1,8 @@
-$( A shortening found by the minimizer.  The comparison with min-not-found.mm
-   suggests that the minimizer's ability to detect this one depends on the
-   presence of statement "A" in at least one of the steps of the minimized
-   proof.  Axiom ax-3 and costant C are not used here, but they are kept
-   anyway to lessen the amount of differences with min-found.mm. $)
+$( A shortening found by the minimizer.  The comparison with min_not_found.mm
+   suggests that the minimizer's ability to detect it depends on the presence
+   of statement "A" in the steps of the minimized proof.  The costant C and
+   axiom ax-3 are not used here, but they are kept anyway to lessen the amount
+   of differences with min_not_found.mm. $)
 
   $c A B C D $.
 

diff --git a/tests/min_not_found.expected b/tests/min_not_found.expected
@@ -1,6 +1,6 @@
 MM> READ "min_not_found.mm"
-Reading source file "min_not_found.mm"... 762 bytes
-762 bytes were read into the source buffer.
+Reading source file "min_not_found.mm"... 787 bytes
+787 bytes were read into the source buffer.
 The source has 18 statements; 5 are $a and 2 are $p.
 SET EMPTY_SUBSTITUTION was turned ON (allowed) for this database.
 No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *

diff --git a/tests/min_not_found.mm b/tests/min_not_found.mm
@@ -1,8 +1,8 @@
-$( A shortening not found by the minimizer.  The comparison with min-found.mm
+$( A shortening not found by the minimizer.  The comparison with min_found.mm
    suggests that the minimizer's inability to detect it is due to the absence
    of statement "C" in any of the steps of the minimized proof.  The
-   shortening is detected if proveFloating is set to 1 in minimizeProof,
-   which allows absent "$e" statements to be found. $)
+   shortening is detected if proveFloating is set to 1 in replaceStatement
+   called by minimizeProof, which allows absent $e statements to be found. $)
 
   $c A B C D $.