# HG changeset patch # User kleing # Date 1059478336 -7200 # Node ID 9b7a62788dac7d17f623b7d74e8dd636c2801b15 # Parent f8a25218b423dd5fea2923bba3c936c2f8f90875 opened new section for next Isabelle release diff -r f8a25218b423 -r 9b7a62788dac NEWS --- a/NEWS Mon Jul 28 11:16:38 2003 +0200 +++ b/NEWS Tue Jul 29 13:32:16 2003 +0200 @@ -4,6 +4,15 @@ New in this Isabelle release ---------------------------- +*** HOL *** + +* 'specification' command added, allowing for definition by +specification. + + +New in Isabelle2003 (May 2003) +-------------------------------- + *** General *** * Provers/simplifier: @@ -110,9 +119,6 @@ *** HOL *** -* 'specification' command added, allowing for definition by -specification. - * arith(_tac) - Produces a counter example if it cannot prove a goal.