merge_prla

Originally this tool is for merging proofs in .prla files, I have extended this util a little that it can now print out proof terms to a readable format, without starting MetaPRL editor.

To compile it, call omake bin/merge_prla in MetaPRL root directory.

An example output (on fol/fol_prop.prla):

Rule/Rewrite distrib_or:
   Proof:
      0 by autoT
        0.1 by dT 2 ta
          0.1.1 by selT 1 (dT 0) ta
            No Subgoals
          Close 0.1.1
        Close 0.1
        0.2 by dT 2 ta
          0.2.1 by selT 2 (dT 0) ta
            No Subgoals
          Close 0.2.1
        Close 0.2
      Close 0
Rule/Rewrite imp_and_rule: Proof: 0 by assertT << 'C => 'D => 'B >> ta
                                    0.1 by dT 2 ta
                                      No Subgoals
                                    Close 0.1
                                  Close 0
Rule/Rewrite imp_or_rule:
   Proof:
      0 by assertT << 'C => 'B >> thenMT assertT << 'D => 'B >> ta
        0.1 by dT 2 ta
          0.1.1 by selT 2 autoT
            No Subgoals
          Close 0.1.1
        Close 0.1
        0.2 by dT 2 ta
          0.2.1 by selT 1 autoT
            No Subgoals
          Close 0.2.1
        Close 0.2
        0.3 by dT 2 ta
          0.3.1 by selT 2 autoT
            No Subgoals
          Close 0.3.1
        Close 0.3
      Close 0
Rule/Rewrite imp_imp_rule: Proof: 0 by assertT <<'D => 'B>> ta
                                    0.1 by dT 2 ta
                                      No Subgoals
                                    Close 0.1
                                  Close 0
Rule/Rewrite distrib_or2:
   Proof:
      0 by autoT
        0.1 by dT 2 ta
          0.1.1 by selT 1 autoT
            No Subgoals
          Close 0.1.1
        Close 0.1
        0.2 by dT 2 ta
          0.2.1 by selT 2 autoT
            No Subgoals
          Close 0.2.1
        Close 0.2
      Close 0