# HG changeset patch
# User traytel
# Date 1474036404 -7200
# Node ID 8947157ca8305b66492e5a21d4f348e140957e9a
# Parent  685fb01256af401d6fea2fd4a73e06812d9df36f
NEWS

diff -r 685fb01256af -r 8947157ca830 NEWS
--- a/NEWS	Fri Sep 16 13:56:51 2016 +0200
+++ b/NEWS	Fri Sep 16 16:33:24 2016 +0200
@@ -332,6 +332,11 @@
   - The MaSh relevance filter has been sped up.
   - Produce syntactically correct Vampire 4.0 problem files.
 
+* The 'coinductive' command produces a proper coinduction rule for
+mutual coinductive predicates. This new rule replaces the old rule,
+which exposed details of the internal fixpoint construction and was
+hard to use. INCOMPATIBILITY.
+
 * (Co)datatype package:
   - New commands for defining corecursive functions and reasoning about
     them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive',