[isabelle-dev] NEWS: eliminated atac, rtac, etac, dtac, ftac

Makarius 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 
by default.


More information about the isabelle-dev mailing list