repaired "Mutabelle" after Refute move

less verbose -- the warning will reach the users anyway by other means

tuned messages

moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong

fixes related to Refute's move

added a timeout around script that relies on the network

took out "using only ..." comments in Sledgehammer generated metis/smt calls, until these can be generated soundly

moved Refute to "HOL/Library" to speed up building "Main" even more

tuning

use metaquantification when possible in Isar proofs

tuned code

tuning

soft SMT timeout

added function store_termination_rule to the signature, as it is used in Nominal2

longer log, to accomodate final status line of isabelle build;

transfer package: error message if preprocessing goal to object-logic formula fails

transfer package: add test to prevent trying to make cterms from open terms

transfer package: more flexible handling of equality relations using is_equality predicate

ensured that rewr_conv rule t = "t == u" literally not just modulo beta-eta

new theorems

incorporated constant chars into instantiation proof for enum; tuned proofs for properties on enum of chars; swapped theory dependency of Enum.thy and String.thy

close code theorems explicitly after preprocessing

tuned proofs;

further attempts to cope with large files via option jedit_text_overview_limit;

more detailed Prover IDE NEWS;

recovered explicit error message, which was lost in b8570ea1ce25;

removed dead code;

proper signatures;

tuned;

merged