@misc{deploy464, month = {November}, title = {Mathematical Language of Event-B Proofs}, author = {Laurent Voisin}, year = {2013}, url = {http://deploy-eprints.ecs.soton.ac.uk/464/}, abstract = {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.} }