(* Lexical concerns: The categories here assume that there is white space between instances of the categories. For the quoted propositions taken as constants, this means that if p is a proposition, then " p " is a constant. Allowing "p" as a constant also is fine, but " p " should be accepted. *) ::= | | | "not" ; ::= '"' '"' ; | ... ; ::= ... ; ::= (* weight is rational in range 0.0 to 1.0 *) ::= "Default proof standard: " ; ::= ::= "If" "then" ; ::= "If" "then" "unless" ; ::= ... (* either single prop, or "and" separated list of props. *) ::= ... (* either single prop, or "or" separated list of props. *) ::= ... ::= ... (* line starting with ## *) ::= ; ::= ; ::= | ":" < argument > ":" | "Assumption:" | "Proof standard:" ":" | "Main query:" ;