Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2008-07-10 19:30:08 -0700 (Thu, 10 Jul 2008)
Revision: 13110
Log message:

      Added some code that extracts and prints all formulas that were claimed tautologies (and left unproven) in the proof.
     Most of these formulas are propositional tautologies and we can check them with JProver (if we like).
     Two other types of tautologies are:
     1. (A,t:A -> C) -> (t:A -> C)
     2. (A->t:B) -> (A->(t1+..+t+..tn):B)
     and variations of these forms (with side formulas from Gentzen-style rules)
     We have to discuss it with SNA, if we want to prove them explicitely or not, anyway it's a minor issue.