(*
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:" ;