dropped idle local_facts argument; factored out theory_abbrev and locale_abbrev

more convenient order

dropped misleading comments

merged

separated foundation of `notes`

more clear separation into local and global facts

sharpened and tuned educated guess for canonical class morphism

minimize sorts in certificate instantiation

prevent ATP thread for staying around for 1 minute if an exception occurred earlier; this is a workaround for what could be a misfeature of "Async_Manager", which I'd rather not touch

adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present

"declare" -> "declaration" (typo)

replace "setup" with "declaration"

disable Nitpick on Cygwin while I'm on vacation; I'll look into the timeout once I'm back

merged

use "declaration" instead of "setup" to register Nitpick extensions

remove needless "open"

move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)

fiddle some more with "max_new_relevant_facts_per_iter"

replace recursion with "fold"

remove debugging output

remove now needless "Thm.transfer"

reintroduced old code that removed axioms from the conjecture assumptions, ported to FOF

merge

fix embarrassing bug in elim rule handling, introduced during the port to FOF

minor doc changes

modernized some specifications;

tuned;

Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;