Isar/Pure: removed obsolete 'transfer' attribute (transfer of thms to
the current context is now done automatically);
--- 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);