Proof Simplification
From Event-B
Proofs stored in xml text files are sometimes quite large (70 MB proof files exist). We know that some information contained in these files is not needed. For instance, rewriting a predicate p1 into p2 when p2 is never used afterwards, is a needless step. This development aims at getting rid of that kind of needless data contained in proof files.
TODO: complete