lemmas about right derivative and limits

lemma about differences of convex functions

lemmas relating ln x and x - 1

use divide instead of inverse for the derivative of ln

adding ISABELLE_GHC environment setting to mira configuration isabelle makeall all on lxbroy10

renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;

document depth arguments of method "auto";

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;

clarified special incr_type_indexes;

tuned signature: Name.invent and Name.invent_names;

modernized structure ProofContext;

even more robust \isaspacing;

simplified Name.variant -- discontinued builtin fold_map;

some attempts at robust \isaspacing so that \isa{...} can be used in section headings etc. (need to avoid `\? for some reason);

discontinued Name.variant to emphasize that this is old-style / indirect;

prefer new-style Name.invents;

more tight name invention -- avoiding old functions;

\frenchspacing for formal isabelle style avoids extra space in situations like ``@{text "?"}'' followed by plain text;

tuned;

NEWS

correcting import theory of examples

fixing code generation test

removing char setup

removing unneccessary manual instantiations and dead definitions; hiding more constants and facts

adding a nicer error message for quickcheck_narrowing; hiding fact empty_def

adding narrowing engine for existentials

adapting Quickcheck_Narrowing: adding setup for characters; correcting import statement

adding theory Quickcheck_Narrowing to HOL-Main image

adapting IsaMakefile

moving Quickcheck_Narrowing from Library to base directory