%A Laurent Voisin
%T Mathematical Language of Event-B Proofs
%X This model proves correct the optimisation implemented in Rodin 3.0 for storing the mathematical language in which proofs are written.

See http://wiki.event-b.org/index.php/Language_of_an_Event-B_Component for more details on the context of this model.
%D 2013
%I Systerel
%L deploy464

<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>