[isabelle-dev] NEWS

[Johannes Hölzl]

* Changed DERIV_intros to a NamedThmsFun. Each of the theorems in
DERIV_intros
assumes composition with an additional function and matches a variable
to the
derivative, which has to be solved by the simplifier. Hence
(auto intro!: DERIV_intros) computes the derivative of most elementary
terms.

* Maclauren.DERIV_tac and Maclauren.deriv_tac was removed, they are
replaced by:
(auto intro!: DERIV_intros)
INCOMPATIBILITY.

DERIV_tac, deriv_tac, and DERIV_intros is not used in AFP. When someone
has private theories using this tactices, could you please try to
replace it with (auto intro!: DERIV_intros)? 

 Johannes