NEWS
changeset 60793 bbcd4ab6d26e
parent 60712 3ba16d28449d
child 60802 067658d63c5d
--- a/NEWS	Sun Jul 26 22:19:14 2015 +0200
+++ b/NEWS	Sun Jul 26 22:26:11 2015 +0200
@@ -244,7 +244,11 @@
 command. Minor INCOMPATIBILITY, use 'function' instead.
 
 
-** ML **
+*** ML ***
+
+* Old tactic shorthands atac, rtac, etac, dtac, ftac have been
+discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc.
+instead (with proper context).
 
 * Thm.instantiate (and derivatives) no longer require the LHS of the
 instantiation to be certified: plain variables are given directly.