Manpage

README.TXT

@@ -127,7 +127,7 @@ you can use "make uninstall" to remove it.
 List of databases
 -----------------
 
-The data base files included are:
+The database files included are:
 
   set.mm - logic and set theory database (see Ch. 3 of the Metamath book).
       The Metamath Proof Explorer pages were generated from this database.

src/metamath.1

@@ -27,7 +27,7 @@ metamath \- Formal proof verifier and proof assistant
 is a formal proof verifier and proof assistant for the Metamath language.
 It can be initialized via a series of
 .I commands
-or with a data base
+or with a database
 .IR file ,
 which can then be explored interactively.
 .PP
@@ -38,10 +38,10 @@ installed along with the package.
 .SH LANGUAGE
 A Metamath database consists of a sequence of three kinds of tokens
 separated by white space (which is any sequence of one or more white
-space characters). The set of keyword tokens is
+space characters).  The set of keyword tokens is
 .BR ${ ", " $} ", " $c ", " $v ", " $f ", " $e ", " $d ", " $a ", " $p ", "
 .BR $. ", " $= ", " $( ", " $) ", " $[ ", and " $] .
-The latter four are called auxiliary or preprocessing keywords. A
+The latter four are called auxiliary or preprocessing keywords.  A
 .I label
 token consists of any combination of letters, digits, and the characters hyphen,
 underscore, and period.
@@ -62,29 +62,29 @@ Include the contents of a
 .IR file .
 .TP
 .BI ${ " statements " $}
-Scoped block of statements. A math symbol becomes active when declared and
+Scoped block of statements.  A math symbol becomes active when declared and
 stays active until the end of the block in which it is declared.
 .TP
 .BI $v " symbols " $.
 Declare
 .I symbols
-as variables. A variable may not be declared a second time while it is active,
+as variables.  A variable may not be declared a second time while it is active,
 but it may be declared again (as a variable, but not as a constant) after it
 becomes inactive.
 .TP
 .BI $c " symbols " $.
 Declare
 .I symbols
-as constants. A constant must be declared in the outermost block and may not be
-declared a second time.
+as constants.  A constant must be declared in the outermost block and may not
+be declared a second time.
 .TP
 .IB "label " $f " constant variable " $.
 Variable-type hypothesis to specify the nature or type of a variable (such as
-`let x be an integer.'). A variable must have its type specified in a
+`let x be an integer.').  A variable must have its type specified in a
 .B $f
 statement before it may be used in a
 .BR $e ", " $a ", or " $p
-statement. There may not be two active
+statement.  There may not be two active
 .B $f
 statements containing the same variable.
 .TP
@@ -93,31 +93,31 @@ Logical hypothesis, expressing a logical truth (such as `assume x is prime')
 that must be established in order for an assertion requiring it to also be true.
 .TP
 .BI $d " variables " $.
-Disjoint variable restriction. For distinct active
+Disjoint variable restriction.  For distinct active
 .IR variables ,
 it forbids the substitution of one variable with another.
 .TP
 .IB "label " $a " constant symbols " $.
 Axiomatic assertion.
 .TP
 .IB "label " $p " constant symbols " $= " proof " $.
-Provable assertion. The
+Provable assertion.  The
 .I proof
 is a sequence of statement
 .IR label s.
 This label sequence serves as a set of instructions that the Metamath program
-uses to construct a series of math symbol sequences. The construction must
+uses to construct a series of math symbol sequences.  The construction must
 ultimately result in the math symbol sequence contained between the
 .BR $p " and " $=
 keywords of the
 .B $p
-statement. For details, see section 4.3 in [1].
+statement.  For details, see section 4.3 in [1].
 Proofs are most easily written using the interactive prompt in
 .BR metamath .
 .SH FILES
 .I /usr/share/metamath
 .RS
-Data base files for several formal theories.
+Database files for several formal theories.
 .SH SEE ALSO
 .B "[1]"
 Norman Megill:

src/metamath.c

@@ -79,7 +79,9 @@
      Remove mmmaci and everything related to THINK_C compiler
    4-Jan-2022 mc - change VERIFY MARKUP /TOP_DATE_SKIP and /FILE_SKIP to
      /TOP_DATE_CHECK and /FILE_CHECK (with opposite meaning), and make the
-     skip behavior the default. */
+     skip behavior the default.
+   7-Sep-2022 bj mmwtex.c, mmhlpa.c Added CRITERIA CRITERION to [bib]
+     keywords */
 /* 0.198 nm 7-Aug-2021 mmpars.c - Fix cosmetic bug in WRITE SOURCE ... /REWRAP
    that prevented end of sentence (e.g. period) from appearing in column 79,
    thus causing some lines to be shorter than necessary. */

src/mmhlpa.c

@@ -1130,11 +1130,11 @@ H("");
 H("The <keyword>, which is not case-sensitive, must be one of the following:");
 H("");
 H("    Axiom, Chapter, Claim, Compare, Conclusion, Condition, Conjecture,");
-H("    Corollary, Definition, Equation, Example, Exercise, Fact, Figure,");
-H("    Introduction, Item, Lemma, Lemmas, Line, Lines, Notation, Note,");
-H("    Observation, Paragraph, Part, Postulate, Problem, Proof, Property,");
-H("    Proposition, Remark, Result, Rule, Scheme, Scolia, Scolion, Section,");
-H("    Statement, Subsection, Table, Theorem");
+H("    Corollary, Criteria, Criterion, Definition, Equation, Example,");
+H("    Exercise, Fact, Figure, Introduction, Item, Lemma, Lemmas, Line,");
+H("    Lines, Notation, Note, Observation, Paragraph, Part, Postulate,");
+H("    Problem, Proof, Property, Proposition, Remark, Result, Rule, Scheme,");
+H("    Scolia, Scolion, Section, Statement, Subsection, Table, Theorem");
 H("");
 H("The <identifier> is optional, as in for example \"Remark in [Monk] p. 22\".");
 H("");

src/mmwtex.c

@@ -5317,6 +5317,8 @@ flag writeBibliography(vstring bibFile,
               || !strcmp(mid(str2, k, (long)strlen("SCOLION")), "SCOLION")
               || !strcmp(mid(str2, k, (long)strlen("SUBSECTION")), "SUBSECTION")
               || !strcmp(mid(str2, k, (long)strlen("TABLE")), "TABLE")
+              || !strcmp(mid(str2, k, (long)strlen("CRITERION")), "CRITERION")
+              || !strcmp(mid(str2, k, (long)strlen("CRITERIA")), "CRITERIA")
               ) {
             m = k;
             break;