Grammar of MML Query

Source: mmlquery.xml
Date: February 20, 2005
Version: 1.0
Initial term: Query-sequence

Contents

  1. General
  2. Queries
  3. Operations
  4. Ordering
  5. Abbreviations
  6. Description
  7. Non-terminals
  8. Terminals

System terms (usage):
Basic-operation*, Decode-type, Grep-options, Grep-pattern, Identifier, MML-version, Mizar-formula, Mizar-symbol, Non-letter, Numeral, Presentation-style, Pure-format, Slash-query-options, String, Symbols-or-keywords.

General


Query-sequence =
( Ordered-query | Abbreviation-declaration ) { ";" ( Ordered-query | Abbreviation-declaration ) } .
use

Ordered-query =
Query [ "ordered" "by" Order-declaration ] [ "select" Selection ] [ "presented" "with" Presentation-style ] .
use

Selection =
Numeral [ "-" Numeral ] { "," Numeral [ "-" Numeral ] } .
use

Queries


Query =
"(" Query ")" | List | Enumerated-list | List-abbreviation | Item-query | Group-query | Fuzzy-query | Compound-query | Filter-query | Selective-query | Context-query | Version-switch-query | Slash-query | Mizar-formula-query .
use

Mizar-formula-query =
"Mizar" ( Mizar-symbol | "(" Mizar-formula ")" ) .
use

Slash-query =
"/" Symbols-or-keywords "/" [ Slash-query-options ] .
use

Version-switch-query =
"version" ( MML-version | ( "+" | "-" ) Numeral ) Query .
use

List =
"list" "of" Resource [ "from" ( Article-name | Article | List | Enumerated-list | List-abbreviation | "(" Query ")" ) ] .
use

Enumerated-list =
"{" [ Item { "," Item } ] "}" | Qualifier "{" [ Non-qualified-item { "," Non-qualified-item } ] "}" .
use

Item-query =
Item .
use

Group-query =
At-least-query | At-most-query | Exactly-query .
use

At-least-query =
( "at" "least" | "atleast" ) [ "minus" Numeral ] [ "*" ] "(" Extended-constructor { "," Extended-constructor } ")" .
use

At-most-query =
( "at" "most" | "atmost" ) [ "plus" Numeral ] [ "*" ] "(" Extended-constructor { "," Extended-constructor } ")" .
use

Exactly-query =
"exactly" { ( "plus" | "minus" ) Numeral } [ "*" ] "(" Extended-constructor { "," Extended-constructor } ")" .
use

Fuzzy-query* =
"fuzzy" [ ( Numeral | "max" | "count" ) [ "-" ( Numeral | "max" | "count" ) ] ] "(" Query { "," Query } ")" .
use

Compound-query =
Query ( "and" | "or" | "butnot" | "but" "not" ) Query .
use

Filter-query =
Prefix-application | Postfix-application .
use

Postfix-application =
Item Operation | Query ( "|" | "&" ) Operation .
use

Prefix-application =
Operation Item | Operation [ ( "|" | "&" ) ] "(" Query ")" .
use

Selective-query =
Query "where" Operation [ ( "<" | "<=" | "=" | ">=" | ">" ) ( Operation | Numeral ) ] .
use

Context-query =
"sequence" [ "in" Decode-type ] "(" [ "/" ] Node { ( "/" | "/*/" | "/+/" ) Node } .
use

Node =
Constructor | String .
use

Resource* =
Library-resource | Qualifier .
use

Library-resource =
"item" | Constructor-resource | Notation-resource | Registration-resource | Statement-resource .
use

Constructor-resource =
"constr" | Constructor-kind .
use

Constructor-kind =
"aggr" | "attr" | "func" | "mode" | "pred" | "sel" | "struct" .
use

Notation-resource =
"notat" | Notation-kind .
use

Notation-kind =
"aggrnot" | "attrnot" | "funcnot" | "modenot" | "prednot" | "selnot" | "structnot" .
use

Registration-resource =
"reg" | Registration-kind .
use

Registration-kind =
"exreg" | "funcreg" | "condreg" .
use

Statement-resource =
"stat" | "thdef" | Statement-kind .
use

Statement-kind =
"th" | "def" | "dfs" | "sch" .
use

Qualifier =
"article" | "symbol" | "format" | "number" | "keyword" | "texmacro" | "version" .
use

Item =
Library-item | Qualified-item | Item-abbreviation .
use

Library-item =
Constructor | Notation | Registration | Statement .
use

Constructor =
Article-name ":" Constructor-kind Numeral .
use

Notation =
Article-name ":" Notation-kind Numeral .
use

Registration =
Article-name ":" Registration-kind Numeral .
use

Statement =
Article-name ":" Statement-kind Numeral .
use

Qualified-item =
Article | Symbol | Format | Number | Keyword | Texmacro .
use

Article =
"article" Article-name .
use

Symbol =
"symbol" String .
use

Format =
"format" Pure-format .
use

Number =
"number" Numeral .
use

Keyword =
"keyword" Identifier .
use

Texmacro =
"texmacro" String .
use

Non-qualified-item =
Identifier | Numeral | Pure-format .
use

Extended-constructor =
Constructor | "fam" Constructor | Number .
use

Article-name =
Identifier .
use

Operations


Operation =
"[" [ "version" ( MML-version | ( "+" | "-" ) Numeral ) ] Compound-operation "]" | Resource-filter | Article-filter | Resource-list | Grep-operation | Reverse-operation | Basic-operation | Identity-operation | Constant-operation | Equality-operation | Membership-operation | Operation-abbreviation .
use

Compound-operation =
Operation | Compound-operation ( "and" | "or" | "butnot" | "but" "not" | "|" | "&" ) Compound-operation | "not" Operation .
use

Resource-filter =
[ "filter" ] Resource .
use

Article-filter =
Article-name ":" "*" .
use

Resource-list =
"all" Resource .
use

Grep-operation =
"grep" [ "-" Grep-options ] Grep-pattern .
use

Reverse-operation =
( "as" | "in" ) Basic-operation .
use

Identity-operation =
"id" .
use

Constant-operation =
"const" "(" Query ")" .
use

Equality-operation =
"=" Item .
use

Membership-operation =
"from" ( "(" Query ")" | Enumerated-list ) .
use

Ordering


Order-declaration =
Order-rule [ "reversed" ] { "," Order-rule [ "reversed" ] } .
use

Order-rule =
Lexical-order | Processing-order | Relative-order | Conditional-order | Counting-order | Iteration-order | Article-order | Resource-order .
use

Lexical-order =
"lexical" "order" .
use

Processing-order =
"processing" "order" .
use

Relative-order =
"value" "of" Relative-operation .
use

Conditional-order =
"first" Condition-operation [ "later" Order-rule ] .
use

Counting-order =
( "count" | "length" | "number" | "quantity" ) "of" Counting-operation .
use

Iteration-order =
"iteration" "of" Iterated-operation .
use

Article-order =
"articles" ( "lexical" | "processing" | "(" Article-name { "," Article-name } ")" ) .
use

Resource-order =
"resources" ( "lexical" | "(" Extended-resource { "," Extended-resource } ")" ) .
use

Relative-operation =
Compound-operation .
use

Condition-operation =
Compound-operation .
use

Counting-operation =
Compound-operation .
use

Iterated-operation =
Compound-operation .
use

Abbreviations


Abbreviation-declaration =
Item-abbreviation-declaration | List-abbreviation-declaration | Operation-abbreviation-declaration | Resource-operation-definition | Collective-abbreviation-declaration | Order-abbreviation-declaration .
use

Item-abbreviation-declaration =
"abbr" Item-abbreviation "=" ( Item | Extended-constructor ) .
use

Item-abbreviation =
Identifier-or-non-letter .
use

List-abbreviation-declaration =
"set" List-abbreviation "=" Query .
use

List-abbreviation* =
"last" | Identifier-or-non-letter .
use

Operation-abbreviation-declaration =
"oper" Operation-abbreviation "=" Operation .
use

Operation-abbreviation =
Identifier-or-non-letter .
use

Resource-operation-definition =
"resource" Extended-resource "operation" "=" Operation .
use

Collective-abbreviation-declaration =
"abbreviations" Abbr-name "to" Abbr-target "from" Scope-query .
use

Order-abbreviation-declaration =
"order" Order-abbreviation "=" Order-rule .
use

Order-abbreviation =
Identifier-or-non-letter .
use

Identifier-or-non-letter =
Identifier | Non-letter .
use

Extended-resource =
Resource | Vocabulary-symbol-kind .
use

Vocabulary-symbol-kind =
"vocG" | "vocK" | "vocL" | "vocM" | "vocO" | "vocR" | "vocU" | "vocV" .
use

Abbr-name =
Operation .
use

Abbr-target =
Operation .
use

Scope-query =
Query .
use

Description

Basic-operation
List of basic operations
Operation Arguments Result Kind Description Examples See also
antecedent Conditional registration Attribute contextual Attributes occurring in antecedent of a given conditional registration positive antecedent, negative antecedent, consequent, cluster
antonym Attribute notation or Predicate notation the same filtering Notation which is antonymous synonym, opposite
article Library item Article classifying Article of the argument
artoccur Article Library item selecting Library items in which occurs at least one constructor from given article occur
associativity Functor the same filtering Functor which is associative
asymmetry Predicate the same filtering Predicate which is asymmetric
baseterm ref Term adjective registration Constructor (or Number!) contextual Constructors occurring in a term whose adjectives are registered
basetype ref Conditional registration or Existential registration Constructor contextual Constructors occurring in a type with which adjectives are registred
by ref Theorem or Scheme or Registration Theorem contextual Theorems used in proofs of given theorem or scheme or correctness conditions of given registration
cluster Registration Attribute contextual Attributes registered in given registration antecedent, consequent, negative cluster, positive cluster
commutativity Functor the same filtering Functor which is commutative
connectedness Predicate the same filtering Predicate which is connected
consequent Conditional registration Attribute contextual Attributes occurring in consequent of a given conditional registration positive consequent, negative consequent, antecedent, cluster
constructor Notation or Definiens Constructor converting Constructor denoted by given notation or definendum of given definiens notation, definiens
copy Constructor Constructor Copies of given constructor if original redef, origin
definiens Constructor Definiens * Definientia of given constractor dfs
definition Constructor Constructor
deftype-ref Constructor Constructor
direct Constructor Constructor
direct-notation Constructor Constructor
expandable-ref Constructor Constructor
extoccur Constructor Library item selecting Library items in which occurs given constructor or its copy ref, occur, artoccur
idempotence Functor the same filtering Functor which is idempotent
intypeattr Constructor Constructor
involutiveness Functor the same filtering Functor which is involution
irreflexivity Predicate the same filtering Predicate which is irreflexive
keyword Constructor Constructor
loci-ref Constructor Constructor
mainfunc Constructor Constructor
mainmode Constructor Constructor
mothertype-ref Constructor Constructor
negative antecedent Conditional registration Attribute contextual Attributes occurring negatively in antecedent of a given conditional registration positive antecedent, antecedent, consequent, cluster
negative cluster Registration Attribute contextual Attributes occurring negatively in given registration consequent, antecedent, positive cluster, cluster
negative consequent Conditional registration Attribute contextual Attributes occurring negatively in consequent of a given conditional registration positive consequent, antecedent, consequent, cluster
negative-intypeattr Constructor Constructor
negative-ref Constructor Constructor
notation Constructor Constructor
occur Constructor Library item selecting Library items in which occurs given constructor ref, artoccur, extoccur
opposite Constructor Constructor
opposite-notation Constructor Constructor
origin Constructor Constructor Origin of given constructor redef, copy
outtypeattr Constructor Constructor
parameter-ref Constructor Constructor
positive antecedent Conditional registration Attribute contextual Attributes occurring positively in antecedent of a given conditional registration antecedent, negative antecedent, consequent, cluster
positive cluster Registration Attribute contextual Attributes occurring positively in given registration antecedent, consequent, negative cluster, cluster
positive consequent Conditional registration Attribute contextual Attributes occurring positively in consequent of a given conditional registration antecedent, negative consequent, consequent, cluster
positive-intypeattr Constructor Constructor
positive-ref Constructor Constructor
positive-occur Constructor Constructor
prefix-ref Constructor Constructor
premise-ref Constructor Constructor
projectivity Functor the same filtering Functor which is projective
redef Constructor Constructor Origin and its copies of given constructor origin, copy
ref Library item Constructor selecting Constructors which occur in given item occur
reflexivity Predicate the same filtering Predicate which is reflexive
symbol Constructor Constructor
symmetry Predicate the same filtering Predicate which is symmetric
synonym Notation the same filtering Notation which is synonymous antonym
termtype-ref Constructor Constructor
texmacro Constructor Constructor
thesis-ref Constructor Constructor
transitivity Predicate the same filtering Predicate which is transitive
translation Constructor Constructor
universe-ref Constructor Constructor
visible Constructor Constructor
vocabulary Symbol Article classifying Vocabulary (article) of the argument

List-abbreviation
The word last refers to last query result.

Fuzzy-query
Fuzzy query conventions
Query/keyword meaning
count the number of subqueries
max the maximal number of subqueries with the same item in answer
fuzzy (Q1,...,Qn) fuzzy max-count (Q1,...,Qn)
fuzzy MIN (Q1,...,Qn) fuzzy MIN-count (Q1,...,Qn)
fuzzy MIN-MAX (Q1,...,Q2) all items which are in at least MIN answers of subqueries and at most in MAX

Resource
Inclusion of resources
Resource Abbreviation Subresources Examples Comments
All Library item, Article, Number, Symbol, Format, Keyword, TeX macro Resource
Library item item Constructor, Notation, Registration, Statement Library-resource
Constructor constr Aggregate, Attribute, Functor, Mode, Predicate, Selector, Structure Constructor-resource, Constructor
Notation notat Aggregate notation, Attribute notation, Functor notation, Mode notation, Predicate notation, Selector notation, Structure notation Notation-resource, Notation
Registration reg Conditional registration, Existential registration, Term adjective registration Registration-resource, Registration
Statement stat Theorem, Definiens, Scheme Statement-resource, Statement
Theorem thdef Regular theorem, Definitional theorem Statement-resource, Statement
Basic resources
Resource Abbreviation Super-resource Examples Comments
Aggregate aggr Constructor Constructor-resource, Constructor
Attribute attr Constructor Constructor-resource, Constructor
Functor func Constructor Constructor-resource, Constructor
Mode mode Constructor Constructor-resource, Constructor
Predicate pred Constructor Constructor-resource, Constructor
Selector sel Constructor Constructor-resource, Constructor
Structure struct Constructor Constructor-resource, Constructor
Aggregate notation aggrnot Notation Constructor-resource, Constructor
Attribute notation attrnot Notation Constructor-resource, Constructor
Functor notation funcnot Notation Constructor-resource, Constructor
Mode notation modenot Notation Constructor-resource, Constructor
Predicate notation prednot Notation Constructor-resource, Constructor
Selector notation selnot Notation Constructor-resource, Constructor
Structure notation structnot Notation Constructor-resource, Constructor
Conditional registration condreg Registration Registration-resource, Registration
Existential registration exreg Registration Registration-resource, Registration
Term adjective registration funcreg Registration Registration-resource, Registration
Regular theorem th Theorem Statement-resource, Statement
Definitional theorem def Theorem Statement-resource, Statement
Definiens dfs Statement Statement-resource, Statement
Scheme sch Statement Statement-resource, Statement
Article article All Qualifier, Article
Number number All Qualifier, Number
Symbol symbol All Qualifier, Symbol
Format format All Qualifier, Format
Keyword keyword All Qualifier, Keyword
TeX macro texmacro All Qualifier, Texmacro

Non-terminals and system-terms

  1. Abbr-name in Collective-abbreviation-declaration,
  2. Abbr-target in Collective-abbreviation-declaration,
  3. Abbreviation-declaration in Query-sequence,
  4. Article in List, Qualified-item,
  5. Article-filter in Operation,
  6. Article-name in List, Constructor, Notation, Registration, Statement, Article, Article-filter, Article-order,
  7. Article-order in Order-rule,
  8. At-least-query in Group-query,
  9. At-most-query in Group-query,
  10. Basic-operation in Operation, Reverse-operation,
  11. Collective-abbreviation-declaration in Abbreviation-declaration,
  12. Compound-operation in Operation, Compound-operation, Compound-operation, Relative-operation, Condition-operation, Counting-operation, Iterated-operation,
  13. Compound-query in Query,
  14. Condition-operation in Conditional-order,
  15. Conditional-order in Order-rule,
  16. Constant-operation in Operation,
  17. Constructor in Node, Library-item, Extended-constructor, Extended-constructor,
  18. Constructor-kind in Constructor-resource, Constructor,
  19. Constructor-resource in Library-resource,
  20. Context-query in Query,
  21. Counting-operation in Counting-order,
  22. Counting-order in Order-rule,
  23. Decode-type in Context-query,
  24. Enumerated-list in Query, List, Membership-operation,
  25. Equality-operation in Operation,
  26. Exactly-query in Group-query,
  27. Extended-constructor in At-least-query, At-most-query, Exactly-query, Item-abbreviation-declaration,
  28. Extended-resource in Resource-order, Resource-operation-definition,
  29. Filter-query in Query,
  30. Format in Qualified-item,
  31. Fuzzy-query in Query,
  32. Grep-operation in Operation,
  33. Grep-options in Grep-operation,
  34. Grep-pattern in Grep-operation,
  35. Group-query in Query,
  36. Identifier in Keyword, Non-qualified-item, Article-name, Identifier-or-non-letter,
  37. Identifier-or-non-letter in Item-abbreviation, List-abbreviation, Operation-abbreviation, Order-abbreviation,
  38. Identity-operation in Operation,
  39. Item in Enumerated-list, Item-query, Postfix-application, Prefix-application, Equality-operation, Item-abbreviation-declaration,
  40. Item-abbreviation in Item, Item-abbreviation-declaration,
  41. Item-abbreviation-declaration in Abbreviation-declaration,
  42. Item-query in Query,
  43. Iterated-operation in Iteration-order,
  44. Iteration-order in Order-rule,
  45. Keyword in Qualified-item,
  46. Lexical-order in Order-rule,
  47. Library-item in Item,
  48. Library-resource in Resource,
  49. List in Query, List,
  50. List-abbreviation in Query, List, List-abbreviation-declaration,
  51. List-abbreviation-declaration in Abbreviation-declaration,
  52. MML-version in Version-switch-query, Operation,
  53. Membership-operation in Operation,
  54. Mizar-formula in Mizar-formula-query,
  55. Mizar-formula-query in Query,
  56. Mizar-symbol in Mizar-formula-query,
  57. Node in Context-query, Context-query,
  58. Non-letter in Identifier-or-non-letter,
  59. Non-qualified-item in Enumerated-list,
  60. Notation in Library-item,
  61. Notation-kind in Notation-resource, Notation,
  62. Notation-resource in Library-resource,
  63. Number in Qualified-item, Extended-constructor,
  64. Numeral in Selection, Selection, Version-switch-query, At-least-query, At-most-query, Exactly-query, Fuzzy-query, Fuzzy-query, Selective-query, Constructor, Notation, Registration, Statement, Number, Non-qualified-item, Operation,
  65. Operation in Postfix-application, Postfix-application, Prefix-application, Prefix-application, Selective-query, Selective-query, Compound-operation, Compound-operation, Operation-abbreviation-declaration, Resource-operation-definition, Abbr-name, Abbr-target,
  66. Operation-abbreviation in Operation, Operation-abbreviation-declaration,
  67. Operation-abbreviation-declaration in Abbreviation-declaration,
  68. Order-abbreviation in Order-abbreviation-declaration,
  69. Order-abbreviation-declaration in Abbreviation-declaration,
  70. Order-declaration in Ordered-query,
  71. Order-rule in Order-declaration, Conditional-order, Order-abbreviation-declaration,
  72. Ordered-query in Query-sequence,
  73. Postfix-application in Filter-query,
  74. Prefix-application in Filter-query,
  75. Presentation-style in Ordered-query,
  76. Processing-order in Order-rule,
  77. Pure-format in Format, Non-qualified-item,
  78. Qualified-item in Item,
  79. Qualifier in Enumerated-list, Resource,
  80. Query in Ordered-query, Query, Version-switch-query, List, Fuzzy-query, Compound-query, Compound-query, Postfix-application, Prefix-application, Selective-query, Constant-operation, Membership-operation, List-abbreviation-declaration, Scope-query,
  81. Query-sequence in ,
  82. Registration in Library-item,
  83. Registration-kind in Registration-resource, Registration,
  84. Registration-resource in Library-resource,
  85. Relative-operation in Relative-order,
  86. Relative-order in Order-rule,
  87. Resource in List, Resource-filter, Resource-list, Extended-resource,
  88. Resource-filter in Operation,
  89. Resource-list in Operation,
  90. Resource-operation-definition in Abbreviation-declaration,
  91. Resource-order in Order-rule,
  92. Reverse-operation in Operation,
  93. Scope-query in Collective-abbreviation-declaration,
  94. Selection in Ordered-query,
  95. Selective-query in Query,
  96. Slash-query in Query,
  97. Slash-query-options in Slash-query,
  98. Statement in Library-item,
  99. Statement-kind in Statement-resource, Statement,
  100. Statement-resource in Library-resource,
  101. String in Node, Symbol, Texmacro,
  102. Symbol in Qualified-item,
  103. Symbols-or-keywords in Slash-query,
  104. Texmacro in Qualified-item,
  105. Version-switch-query in Query,
  106. Vocabulary-symbol-kind in Extended-resource

Terminals

  1. & in Postfix-application, Prefix-application, Compound-operation,
  2. ( in Query, Mizar-formula-query, List, At-least-query, At-most-query, Exactly-query, Fuzzy-query, Prefix-application, Context-query, Constant-operation, Membership-operation, Article-order, Resource-order,
  3. ) in Query, Mizar-formula-query, List, At-least-query, At-most-query, Exactly-query, Fuzzy-query, Prefix-application, Constant-operation, Membership-operation, Article-order, Resource-order,
  4. * in At-least-query, At-most-query, Exactly-query, Article-filter,
  5. + in Version-switch-query, Operation,
  6. , in Selection, Enumerated-list, Enumerated-list, At-least-query, At-most-query, Exactly-query, Fuzzy-query, Order-declaration, Article-order, Resource-order,
  7. - in Selection, Version-switch-query, Fuzzy-query, Operation, Grep-operation,
  8. / in Slash-query, Slash-query, Context-query, Context-query,
  9. /*/ in Context-query,
  10. /+/ in Context-query,
  11. : in Constructor, Notation, Registration, Statement, Article-filter,
  12. ; in Query-sequence,
  13. < in Selective-query,
  14. <= in Selective-query,
  15. = in Selective-query, Equality-operation, Item-abbreviation-declaration, List-abbreviation-declaration, Operation-abbreviation-declaration, Resource-operation-definition, Order-abbreviation-declaration,
  16. > in Selective-query,
  17. >= in Selective-query,
  18. Mizar in Mizar-formula-query,
  19. [ in Operation,
  20. ] in Operation,
  21. abbr in Item-abbreviation-declaration,
  22. abbreviations in Collective-abbreviation-declaration,
  23. aggr in Constructor-kind,
  24. aggrnot in Notation-kind,
  25. all in Resource-list,
  26. and in Compound-query, Compound-operation,
  27. article in Qualifier, Article,
  28. articles in Article-order,
  29. as in Reverse-operation,
  30. at in At-least-query, At-most-query,
  31. atleast in At-least-query,
  32. atmost in At-most-query,
  33. attr in Constructor-kind,
  34. attrnot in Notation-kind,
  35. but in Compound-query, Compound-operation,
  36. butnot in Compound-query, Compound-operation,
  37. by in Ordered-query,
  38. condreg in Registration-kind,
  39. const in Constant-operation,
  40. constr in Constructor-resource,
  41. count in Fuzzy-query, Fuzzy-query, Counting-order,
  42. def in Statement-kind,
  43. dfs in Statement-kind,
  44. exactly in Exactly-query,
  45. exreg in Registration-kind,
  46. fam in Extended-constructor,
  47. filter in Resource-filter,
  48. first in Conditional-order,
  49. format in Qualifier, Format,
  50. from in List, Membership-operation, Collective-abbreviation-declaration,
  51. func in Constructor-kind,
  52. funcnot in Notation-kind,
  53. funcreg in Registration-kind,
  54. fuzzy in Fuzzy-query,
  55. grep in Grep-operation,
  56. id in Identity-operation,
  57. in in Context-query, Reverse-operation,
  58. item in Library-resource,
  59. iteration in Iteration-order,
  60. keyword in Qualifier, Keyword,
  61. last in List-abbreviation,
  62. later in Conditional-order,
  63. least in At-least-query,
  64. length in Counting-order,
  65. lexical in Lexical-order, Article-order, Resource-order,
  66. list in List,
  67. max in Fuzzy-query, Fuzzy-query,
  68. minus in At-least-query, Exactly-query,
  69. mode in Constructor-kind,
  70. modenot in Notation-kind,
  71. most in At-most-query,
  72. not in Compound-query, Compound-operation, Compound-operation,
  73. notat in Notation-resource,
  74. number in Qualifier, Number, Counting-order,
  75. of in List, Relative-order, Counting-order, Iteration-order,
  76. oper in Operation-abbreviation-declaration,
  77. operation in Resource-operation-definition,
  78. or in Compound-query, Compound-operation,
  79. order in Lexical-order, Processing-order, Order-abbreviation-declaration,
  80. ordered in Ordered-query,
  81. plus in At-most-query, Exactly-query,
  82. pred in Constructor-kind,
  83. prednot in Notation-kind,
  84. presented in Ordered-query,
  85. processing in Processing-order, Article-order,
  86. quantity in Counting-order,
  87. reg in Registration-resource,
  88. resource in Resource-operation-definition,
  89. resources in Resource-order,
  90. reversed in Order-declaration,
  91. sch in Statement-kind,
  92. sel in Constructor-kind,
  93. select in Ordered-query,
  94. selnot in Notation-kind,
  95. sequence in Context-query,
  96. set in List-abbreviation-declaration,
  97. stat in Statement-resource,
  98. struct in Constructor-kind,
  99. structnot in Notation-kind,
  100. symbol in Qualifier, Symbol,
  101. texmacro in Qualifier, Texmacro,
  102. th in Statement-kind,
  103. thdef in Statement-resource,
  104. to in Collective-abbreviation-declaration,
  105. value in Relative-order,
  106. version in Version-switch-query, Qualifier, Operation,
  107. vocG in Vocabulary-symbol-kind,
  108. vocK in Vocabulary-symbol-kind,
  109. vocL in Vocabulary-symbol-kind,
  110. vocM in Vocabulary-symbol-kind,
  111. vocO in Vocabulary-symbol-kind,
  112. vocR in Vocabulary-symbol-kind,
  113. vocU in Vocabulary-symbol-kind,
  114. vocV in Vocabulary-symbol-kind,
  115. where in Selective-query,
  116. with in Ordered-query,
  117. { in Enumerated-list, Enumerated-list,
  118. | in Postfix-application, Prefix-application, Compound-operation,
  119. } in Enumerated-list, Enumerated-list
Grzegorz Bancerek, bancerek@mizar.org
Done with grammar2thtml.xsl 8/10/03