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.