[isabelle-dev] NEWS: eliminated atac, rtac, etac, dtac, ftac
makarius at sketis.net
Mon Jul 27 22:32:56 CEST 2015
* Old tactic shorthands atac, rtac, etac, dtac, ftac have been
discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc.
instead (with proper context).
This refers to Isabelle/bbcd4ab6d26e. It is rather unspectacular, but the
practical consequence is a better chance that context discipline is right
More information about the isabelle-dev