We have now a parser that can read a propositional calculus proof written in ASCII text format and transform it into a QEDEQ XML NODE element. It was quickly hacked together but enables us to speed up proof integration. It can be accessed via GUI menu entry "Tools / Proof Text to QEDEQ". A derivation rule has now a version too and name plus version must be unique (which is checked). We introduce a "brief" parameter for LaTeX and UTF-8 plugin to produce summary documents.
And last but not least we included more propositions with formal proofs in http://www.qedeq.org/0_04_04/doc/math/qedeq_formal_logic_v1_en.pdf