Isar/Pure: removed obsolete 'transfer' attribute (transfer of thms to
authorwenzelm
Wed, 31 May 2000 14:30:28 +0200
changeset 9011 0cfc347f8d19
parent 9010 ce78dc5e1a73
child 9012 d1bd2144ab5d
Isar/Pure: removed obsolete 'transfer' attribute (transfer of thms to the current context is now done automatically);
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);