I am deploying a system wich write theorems and need to use the subgoals of their prooves as feedback. So I need to parse these subgoals. Someone knows a Parser ready to do this or a grammar for JavaCC or any other CC (preferably for Java)? There is a better way to do this feedback that launch in batch mode with a strategy that shows all subgoals and parse them? Thanks, Brian.