NEWS
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);