changeset 9011 | 0cfc347f8d19 |
parent 8994 | 803533fbb3ec |
child 9028 | 8a1ec8f05f14 |
--- 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);