diff -r ce78dc5e1a73 -r 0cfc347f8d19 NEWS --- a/NEWS Wed May 31 14:29:42 2000 +0200 +++ b/NEWS Wed May 31 14:30:28 2000 +0200 @@ -92,6 +92,9 @@ * Pure: the local context of (non-atomic) goals is provided via case name 'antecedent'; +* Pure: removed obsolete 'transfer' attribute (transfer of thms to the +current context is now done automatically); + * Provers: splitter support (via 'split' attribute and 'simp' method modifier); 'simp' method: 'only:' modifier removes loopers as well (including splits);