src/Provers/typedsimp.ML
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-12-20 wenzelm 2014-12-20 proper context for "net" tactics; avoid implicit Tactic.build_net -- make its operational behavior explicit in application;
2014-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2011-11-28 wenzelm 2011-11-28 avoid stepping outside of context -- plain zero_var_indexes should be sufficient;
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-10-29 wenzelm 2009-10-29 eliminated some old folds;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-10-17 wenzelm 2009-10-17 explicitly qualify Drule.standard;
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
1993-09-16 clasohm 1993-09-16 Initial revision