--- 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 ***