#331 Optimize Formula Factory storage in proof files

[Nicolas Beauger]

Since Rodin 3.0, formula factories are stored in proofs.
One formula factory is serialized for every proof, which can be greedy in disk space.
As an optimization, the most common factory, if any, could be factorized at the root of the proof file.
As another option, all formula factories could be saved outside proofs, with an identifier that would simply be referenced by each proof.

[Son Hoang]

Insteads of storing all formula factories outside the proofs, we can store the "datatype definitions", "operator definitions", etc. outside the proofs (e.g., in a special element for the bpr. proof file). For each proofs, the formula factory can reference these definitions.
Cheers,
Son