hoelzl [Tue, 31 May 2011 21:33:49 +0200] rev 43335
use divide instead of inverse for the derivative of ln
bulwahn [Thu, 09 Jun 2011 11:57:39 +0200] rev 43334
adding ISABELLE_GHC environment setting to mira configuration isabelle makeall all on lxbroy10
wenzelm [Thu, 09 Jun 2011 23:12:02 +0200] rev 43333
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm [Thu, 09 Jun 2011 22:25:25 +0200] rev 43332
document depth arguments of method "auto";
wenzelm [Thu, 09 Jun 2011 22:13:21 +0200] rev 43331
clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
uniform handling of exceptions in depth_tac and blast_tac, discontinued separate blast_depth_tac;
tuned blast_tac: atomize prems only once, outside DEEPEN;
wenzelm [Thu, 09 Jun 2011 20:56:08 +0200] rev 43330
clarified special incr_type_indexes;