diff --git a/README.TXT b/README.TXT index 62791276..95022b73 100644 --- a/README.TXT +++ b/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. diff --git a/src/metamath.1 b/src/metamath.1 index 6d3cab75..0cb1b2bd 100644 --- a/src/metamath.1 +++ b/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,7 +93,7 @@ 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 @@ -101,23 +101,23 @@ it forbids the substitution of one variable with another. 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: diff --git a/src/metamath.c b/src/metamath.c index ed7c206d..59a2372d 100644 --- a/src/metamath.c +++ b/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. */ diff --git a/src/mmhlpa.c b/src/mmhlpa.c index e0c8cfa3..33d63250 100644 --- a/src/mmhlpa.c +++ b/src/mmhlpa.c @@ -1130,11 +1130,11 @@ H(""); H("The , 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 is optional, as in for example \"Remark in [Monk] p. 22\"."); H(""); diff --git a/src/mmwtex.c b/src/mmwtex.c index 2c4e6647..b8d71bfe 100644 --- a/src/mmwtex.c +++ b/src/mmwtex.c @@ -5271,25 +5271,31 @@ flag writeBibliography(vstring bibFile, /* (The string search below is rather inefficient; maybe improve the algorithm if speed becomes a problem.) */ for (k = j - 1; k >= 1; k--) { - /* **IMPORTANT** Make sure to update mmhlpb.c HELP WRITE BIBLIOGRAPHY + /* **IMPORTANT** Make sure to update mmhlpa.c HELP WRITE BIBLIOGRAPHY if new items are added to this list. */ if (0 - /* Put the most frequent ones first to speed up search; - TODO: count occurrences in mmbiblio.html to find optimal order */ + /* The first five keywords are more frequent so are put first for + efficiency; the rest is in alphabetical order. */ || !strcmp(mid(str2, k, (long)strlen("THEOREM")), "THEOREM") || !strcmp(mid(str2, k, (long)strlen("EQUATION")), "EQUATION") || !strcmp(mid(str2, k, (long)strlen("DEFINITION")), "DEFINITION") || !strcmp(mid(str2, k, (long)strlen("LEMMA")), "LEMMA") || !strcmp(mid(str2, k, (long)strlen("EXERCISE")), "EXERCISE") + // ---- end of optimized search ----- || !strcmp(mid(str2, k, (long)strlen("AXIOM")), "AXIOM") - || !strcmp(mid(str2, k, (long)strlen("CLAIM")), "CLAIM") || !strcmp(mid(str2, k, (long)strlen("CHAPTER")), "CHAPTER") + || !strcmp(mid(str2, k, (long)strlen("CLAIM")), "CLAIM") || !strcmp(mid(str2, k, (long)strlen("COMPARE")), "COMPARE") + || !strcmp(mid(str2, k, (long)strlen("CONCLUSION")), "CONCLUSION") || !strcmp(mid(str2, k, (long)strlen("CONDITION")), "CONDITION") || !strcmp(mid(str2, k, (long)strlen("CONJECTURE")), "CONJECTURE") || !strcmp(mid(str2, k, (long)strlen("COROLLARY")), "COROLLARY") + || !strcmp(mid(str2, k, (long)strlen("CRITERIA")), "CRITERIA") + || !strcmp(mid(str2, k, (long)strlen("CRITERION")), "CRITERION") || !strcmp(mid(str2, k, (long)strlen("EXAMPLE")), "EXAMPLE") + || !strcmp(mid(str2, k, (long)strlen("FACT")), "FACT") || !strcmp(mid(str2, k, (long)strlen("FIGURE")), "FIGURE") + || !strcmp(mid(str2, k, (long)strlen("INTRODUCTION")), "INTRODUCTION") || !strcmp(mid(str2, k, (long)strlen("ITEM")), "ITEM") || !strcmp(mid(str2, k, (long)strlen("LEMMAS")), "LEMMAS") || !strcmp(mid(str2, k, (long)strlen("LINE")), "LINE") @@ -5297,24 +5303,21 @@ flag writeBibliography(vstring bibFile, || !strcmp(mid(str2, k, (long)strlen("NOTATION")), "NOTATION") || !strcmp(mid(str2, k, (long)strlen("NOTE")), "NOTE") || !strcmp(mid(str2, k, (long)strlen("OBSERVATION")), "OBSERVATION") + || !strcmp(mid(str2, k, (long)strlen("PARAGRAPH")), "PARAGRAPH") || !strcmp(mid(str2, k, (long)strlen("PART")), "PART") || !strcmp(mid(str2, k, (long)strlen("POSTULATE")), "POSTULATE") || !strcmp(mid(str2, k, (long)strlen("PROBLEM")), "PROBLEM") + || !strcmp(mid(str2, k, (long)strlen("PROOF")), "PROOF") || !strcmp(mid(str2, k, (long)strlen("PROPERTY")), "PROPERTY") || !strcmp(mid(str2, k, (long)strlen("PROPOSITION")), "PROPOSITION") || !strcmp(mid(str2, k, (long)strlen("REMARK")), "REMARK") || !strcmp(mid(str2, k, (long)strlen("RESULT")), "RESULT") || !strcmp(mid(str2, k, (long)strlen("RULE")), "RULE") || !strcmp(mid(str2, k, (long)strlen("SCHEME")), "SCHEME") - || !strcmp(mid(str2, k, (long)strlen("SECTION")), "SECTION") - || !strcmp(mid(str2, k, (long)strlen("PROOF")), "PROOF") - || !strcmp(mid(str2, k, (long)strlen("STATEMENT")), "STATEMENT") - || !strcmp(mid(str2, k, (long)strlen("CONCLUSION")), "CONCLUSION") - || !strcmp(mid(str2, k, (long)strlen("FACT")), "FACT") - || !strcmp(mid(str2, k, (long)strlen("INTRODUCTION")), "INTRODUCTION") - || !strcmp(mid(str2, k, (long)strlen("PARAGRAPH")), "PARAGRAPH") || !strcmp(mid(str2, k, (long)strlen("SCOLIA")), "SCOLIA") || !strcmp(mid(str2, k, (long)strlen("SCOLION")), "SCOLION") + || !strcmp(mid(str2, k, (long)strlen("SECTION")), "SECTION") + || !strcmp(mid(str2, k, (long)strlen("STATEMENT")), "STATEMENT") || !strcmp(mid(str2, k, (long)strlen("SUBSECTION")), "SUBSECTION") || !strcmp(mid(str2, k, (long)strlen("TABLE")), "TABLE") ) {