added Mirabelle to NEWS
authorboehmes
Fri Aug 21 13:38:57 2009 +0200 (2009-08-21)
changeset 32388b23a4326b9bb
parent 32387 e1ebd4d5d181
child 32389 cb3c5189ea85
child 32405 48786f277130
added Mirabelle to NEWS
NEWS
     1.1 --- a/NEWS	Fri Aug 21 13:25:05 2009 +0200
     1.2 +++ b/NEWS	Fri Aug 21 13:38:57 2009 +0200
     1.3 @@ -18,6 +18,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* New testing tool "Mirabelle" for automated (proof) tools. Applies several
     1.8 +tools and tactics like sledgehammer, metis, or quickcheck, to every proof step
     1.9 +in a theory. To be used in batch mode via "isabelle mirabelle".
    1.10 +
    1.11  * New proof method "sos" (sum of squares) for nonlinear real arithmetic
    1.12  (originally due to John Harison). It requires Library/Sum_Of_Squares.
    1.13  It is not a complete decision procedure but works well in practice