--- a/CONTRIBUTORS Wed Oct 02 15:13:41 2013 +0200
+++ b/CONTRIBUTORS Wed Oct 02 15:53:20 2013 +0200
@@ -9,6 +9,9 @@
* September 2013: Nik Sultana, University of Cambridge
Improvements to HOL/TPTP parser and import facilities.
+* September 2013: Johannes Hölzl and Dmitriy Traytel, TUM
+ New "coinduction" method (residing in HOL-BNF) to avoid boilerplate.
+
* Summer 2013: Makarius Wenzel, Université Paris-Sud / LRI
Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.
--- a/NEWS Wed Oct 02 15:13:41 2013 +0200
+++ b/NEWS Wed Oct 02 15:53:20 2013 +0200
@@ -156,6 +156,7 @@
- Various improvements to BNF-based (co)datatype package, including new
commands "primrec_new", "primcorec", and "datatype_new_compat",
as well as documentation. See "datatypes.pdf" for details.
+ - New "coinduction" method to avoid some boilerplate (compared to coinduct).
- Renamed keywords:
data ~> datatype_new
codata ~> codatatype