Version 2.51 (30/07/2009) Compatible with previous version: Yes New features Change of default language to English Version 2.5 (04/05/2009) Compatible with previous version: Yes New features Multiple Developments Proof Obligation Development Integration with the VeriT Theorem Prover New Refinement Laws Help Improvement Fixed minor Bugs Inclusion of a full case study Version 2.4 (17/09/2008) Compatible with previous version: Yes New features New feature: Copy to Clipboard for all windows New refinement laws New help Fixed minor bugs Version 2.3 (13/06/2008) Compatible with previous version: Yes New features Updated Docgenerator with new circus.sty e zed.sty Adding new program paragraph ProgressBar for opening development and Unicod/Latex swap Proof discharge for syntactic restrictions on law applications Marking proof as manual proof (true or false) Internal optimization for loading programs and updating GUI Optimization of law splitting law (less arguments required) New schema laws Better treatment of exceptions Version 2.2 (03/04/2008) Compatible with previous version: Yes New features Fixes a couple of bugs in proof obligation discharge Version 2.1 (02/04/2008) Compatible with previous version: No New features Fixes a couple of bugs in pretty-printing Reduced file size for saved developments Inclusion of GUI facilities Law classification Show proof obligation status Show expansion of some proof obligations Discharge of some proof obligations Annotation of proof obligations Version 2.0 (24/10/2007) Compatible with previous version: No New features Use of new the Circus parser Inclusion of development management facilities Undo/Redo refinement steps Save/Open developments Inclusion of GUI facilities Pretty-printing Filtering applicable laws according to the selected program Add/Read comments in developments Generate LaTeX file documenting developments