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

Makarius makarius at sketis.net
Mon Jul 27 22:32:56 CEST 2015

Previous message (by thread): [isabelle-dev] goals inserts facts into goal statement
Next message (by thread): [isabelle-dev] NEWS: instantiation rules
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

* 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.


 	Makarius

Previous message (by thread): [isabelle-dev] goals inserts facts into goal statement
Next message (by thread): [isabelle-dev] NEWS: instantiation rules
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

More information about the isabelle-dev mailing list