| changeset 63116 | 32492105b015 |
| parent 63113 | fe31996e3898 |
| child 63118 | 80c361e9d19d |
--- a/NEWS Mon May 23 15:46:30 2016 +0100 +++ b/NEWS Mon May 23 18:04:45 2016 +0200 @@ -95,6 +95,9 @@ has been removed for output. It is retained for input only, until it is eliminated altogether. +* Sledgehammer: + - Produce syntactically correct Vampire 4.0 problem files. + * (Co)datatype package: - New commands for defining corecursive functions and reasoning about them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive',