3 Reference
3.1 The Rodin Platform
3.1.1 Eclipse in General
3.1.2 The Event-B Perspective
3.1.3 Customizing a perspective suitable for RODIN
3.1.4 The Event-B Editor
3.1.5 The Structural Event-B Editor
3.1.6 Wizards
3.1.7 The Proving Perspective
3.1.8 Preferences
3.2 Event-B’s modelling notation
3.2.1 About the notation that we use
3.2.2 Contexts
3.2.3 Machines
3.2.4 Well-definedness proof obligations
3.2.5 Theorems
3.2.6 Generated proof obligations
3.2.7 Visibility of identifiers
3.3 Mathematical Notation
3.3.1 Introduction
3.3.2 Predicates
3.3.3 Booleans
3.3.4 Sets
3.3.5 Relations
3.3.6 Arithmetic
3.3.7 Typing
3.3.8 Assignments
3.4 Proving
3.4.1 Sequents
3.4.2 Proof Rules
3.4.3 Proof Tactics
3.4.4 Provers
3.4.5 How to Use the Provers Effectively
3.4.6 Reasoners
3.4.7 Purging Proofs