removed "atp" and "atps" aliases, which users should have forgotten by now if they ever used them

fewer monomorphic instances are necessary, thanks to Sascha's new monomorphizer -- backed up by Judgment Day

compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time

use existing ghc on macbroy20;

local gensym based on Name.variant; do not export internals by default;

uniform use of flexflex_rule;

tuned name (cf. blast_stats);

more official options blast_trace, blast_stats;

merged

merged

resolving an issue with class instances that are pseudo functions in the OCaml code serializer

merged

fixed document generation for HOL

lemma: independence is equal to mutual information = 0

jensens inequality

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;