Update news for Copilot 3.13. Refs #45.

home.md

@@ -1,5 +1,5 @@
 ## News
-**Release 3.12 -- 2022-11-07**
+**Release 3.13 -- 2023-01-07**
 
 We are pleased to announce the release of Copilot 3.12, a stream-based DSL for
 writing and monitoring embedded C programs, with an emphasis on correctness and
@@ -10,26 +10,9 @@ clocks and voting algorithms.
 Among others, Copilot has been used at the Safety Critical Avionics Systems
 Branch of NASA Langley Research Center for monitoring test flights of drones.
 
-The main changes in this release are as follows:
-
-- A new library `copilot-prettyprinter` exposes functions related to the
-  Copilot Core pretty-printing backend. Pre-existing functions included as
-  part of `copilot-core` are now deprecated.
-- The C99 backend now produces an additional header file with struct
-  declarations. This file is used by the C implementation file generated by
-  Copilot to define structs before the declarations of the handlers, avoiding
-  potential forward declarations that the C compiler cannot resolve. Users of
-  Copilot can choose to import the same new type declaration header file before
-  the standard Copilot header file in their hand-written code, or use external
-  definitions that declare compatible structs. Note that, in the former case,
-  the header file that declares the structs must be included *before* the
-  header file that declares the externs, handlers and step function.
-- The custom type equality module in `copilot-core` is now deprecated in favor
-  of the definition of type equality in `base`.
-- `copilot-theorem` now includes support for proofs by bisimulation necessary
-  for future extensions to Copilot.
-- `copilot-core` now complies with the coding rules established as part of the
-  process of compliance with NASA's Class D requirements (NPR 7150.2).
+This release fixes 4 bugs in `copilot-core` and `copilot-c99`. We have also
+removed 2 deprecated modules and one dependency. The new release has been
+published on hackage, as well as github.
 
 This release also continues to use our new software engineering process
 designed to meet the requirements to obtain NASA's Class D software