# HG changeset patch
# User traytel
# Date 1380722000 -7200
# Node ID 4edfd0fd55369eab9ec2303bd41feacc54218dea
# Parent  4d087a8950f39692420854d21bb04622e2f59395
NEWS and CONTRIBUTORS

diff -r 4d087a8950f3 -r 4edfd0fd5536 CONTRIBUTORS
--- 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.
 
diff -r 4d087a8950f3 -r 4edfd0fd5536 NEWS
--- 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