A grammar to parse a declarative proof language including a formula
parser that extends its operator table at runtime. The parser has been
tested with AntLR 3.3. For an example theory file, see settheory.omt


Feel free to adapt the parser according to your needs.


Dominik Dietrich.