2011-06-09 hoelzl [Thu, 09 Jun 2011 14:04:34 +0200] rev 43340
lemma: independence is equal to mutual information = 0
src/HOL/Probability/Independent_Family.thy src/HOL/Probability/Information.thy src/HOL/Probability/Probability_Measure.thy src/HOL/Probability/Radon_Nikodym.thy

2011-06-09 hoelzl [Thu, 09 Jun 2011 13:55:11 +0200] rev 43339
jensens inequality
src/HOL/Probability/Lebesgue_Integration.thy src/HOL/Probability/Probability_Measure.thy

2011-06-09 hoelzl [Thu, 09 Jun 2011 11:50:16 +0200] rev 43338
lemmas about right derivative and limits
src/HOL/Multivariate_Analysis/Derivative.thy src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy

2011-06-09 hoelzl [Thu, 09 Jun 2011 11:50:16 +0200] rev 43337
lemma about differences of convex functions
src/HOL/Library/Convex.thy

2011-06-09 hoelzl [Thu, 09 Jun 2011 11:50:16 +0200] rev 43336
lemmas relating ln x and x - 1
src/HOL/Ln.thy

2011-05-31 hoelzl [Tue, 31 May 2011 21:33:49 +0200] rev 43335
use divide instead of inverse for the derivative of ln
src/HOL/Transcendental.thy

2011-06-09 bulwahn [Thu, 09 Jun 2011 11:57:39 +0200] rev 43334
adding ISABELLE_GHC environment setting to mira configuration isabelle makeall all on lxbroy10
Admin/mira.py

2011-06-09 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;
src/HOL/Decision_Procs/ferrante_rackoff.ML src/HOL/Import/proof_kernel.ML src/HOL/Import/shuffler.ML src/HOL/Library/reflection.ML src/HOL/Multivariate_Analysis/normarith.ML src/HOL/Tools/Metis/metis_reconstruct.ML src/HOL/Tools/Qelim/cooper.ML src/HOL/Tools/Quickcheck/random_generators.ML src/HOL/Tools/Quotient/quotient_tacs.ML src/HOL/Tools/TFL/rules.ML src/HOL/Tools/lin_arith.ML src/HOL/Tools/split_rule.ML src/Provers/hypsubst.ML src/Pure/Isar/rule_insts.ML src/Pure/conv.ML src/Pure/drule.ML src/Tools/induct.ML src/ZF/Tools/cartprod.ML src/ZF/Tools/inductive_package.ML

2011-06-09 wenzelm [Thu, 09 Jun 2011 22:25:25 +0200] rev 43332
document depth arguments of method "auto";
doc-src/IsarRef/Thy/Generic.thy doc-src/IsarRef/Thy/document/Generic.tex

2011-06-09 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;
src/Provers/blast.ML src/Provers/clasimp.ML