Prototype introiff option for find_theorems.

This feature was suggested by Jeremy Avigad / Tobias Nipkow.

It adds an introiff keyword for find_theorems that returns, in
addition to the usual results for intro, any theorems of the
form ([| ... |] ==> (P = Q)) where either P or Q matches the
conclusions of the current goal. Such theorems can be made
introduction rules with [THEN iffDx].

The current patch is for evaluation only. It assumes an
(op = : 'a -> 'a -> bool) operator, which is specific to HOL.
It is not clear how this should be generalised.

replace cont2cont_apply with cont_apply; add new cont2cont lemmas

compatible with preorder; bot and top instances

updated generated files etc/isar-keywords.el and lib/jedit/isabelle.xml

tuned

added Philipp Meyer's implementation of AtpMinimal
together with related changes in the sledgehammer-interface:
adapted type of prover, optional relevance filtering,
public get_prover for registered atps in AtpManager,
included atp_minimize in s/h response;

removed code_name module

desymbolization with case selection

dropped duplicate lemma sum_nonneg_eq_zero_iff

fixed broken link