# HG changeset patch
# User wenzelm
# Date 1134498726 -3600
# Node ID 651438736fa1078bb55340edea9eea329c1ef828
# Parent  5d63a8b35688628ac0ea9c6a25934818fb282284
Provers/induct: coinduct;
HOL/Library: theory Coinductive_List;

diff -r 5d63a8b35688 -r 651438736fa1 NEWS
--- a/NEWS	Tue Dec 13 19:32:05 2005 +0100
+++ b/NEWS	Tue Dec 13 19:32:06 2005 +0100
@@ -115,7 +115,7 @@
   proof (induct n fixing: thesis)
     case 0
     obtain x where "P 0 x" and "Q 0 x" sorry
-    then show thesis by (rule "0.prems")
+    then show thesis by (rule 0)
   next
     case (Suc n)
     obtain x where "P n x" and "Q n x" by (rule Suc.hyps)
@@ -127,6 +127,9 @@
 of the formal thesis parameter, in order to the get the whole
 existence statement through the induction as expected.
 
+* Provers/induct: support coinduction as well.  See
+src/HOL/Library/Coinductive_List.thy for various examples.
+
 * Input syntax now supports dummy variable binding "%_. b", where the
 body does not mention the bound variable.  Note that dummy patterns
 implicitly depend on their context of bounds, which makes "{_. _}"
@@ -154,6 +157,9 @@
 "=" on type bool) are handled, variable names of the form "lit_<n>"
 are no longer reserved, significant speedup.
 
+* Library: added theory Coinductive_List of potentially infinite lists as
+greatest fixed-point.
+
 
 *** ML ***