NEWS
authortraytel
Fri Sep 16 16:33:24 2016 +0200 (2016-09-16)
changeset 638918947157ca830
parent 63886 685fb01256af
child 63892 c17733350344
NEWS
NEWS
     1.1 --- a/NEWS	Fri Sep 16 13:56:51 2016 +0200
     1.2 +++ b/NEWS	Fri Sep 16 16:33:24 2016 +0200
     1.3 @@ -332,6 +332,11 @@
     1.4    - The MaSh relevance filter has been sped up.
     1.5    - Produce syntactically correct Vampire 4.0 problem files.
     1.6  
     1.7 +* The 'coinductive' command produces a proper coinduction rule for
     1.8 +mutual coinductive predicates. This new rule replaces the old rule,
     1.9 +which exposed details of the internal fixpoint construction and was
    1.10 +hard to use. INCOMPATIBILITY.
    1.11 +
    1.12  * (Co)datatype package:
    1.13    - New commands for defining corecursive functions and reasoning about
    1.14      them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive',