combine declaration and definition of foundation constant

more appropriate outline of `define`

backlink definition to target `notes`

merged

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;

native Isabelle_Process commands, based on efficient byte channel protocol for string lists; misc clarification of proc/pid state, eliminated closing flag; misc tuning and simplification;

proper handling of empty text; more informative exceptions;

more uniform XML/YXML string_of_body/string_of_tree;

type XML.Body as basic data representation language (Scala version); tuned;

type XML.body as basic data representation language; tuned;

renamed YXML.binary_text to YXML.escape_controls to emphasize what it actually does;

added string_bytes convenience;

tuned;

removed obsolete methods for (ML) commands;

prefer Nimbus look and feel on all platforms, instead of the somewhat ugly javax.swing.plaf.metal.MetalLookAndFeel, which presumably is implicit fall-back nonetheless;

edit_document: synchronous reply to ensure consistent state wrt. calling (AWT) thread;

distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names; asynchronous Isabelle_Process.init -- raw ML toplevel stays active; simplified Isabelle_Process using actors; misc tuning;

added Library.thread_actor -- thread as actor;

clarified JEDIT_JAVA_OPTIONS vs. JEDIT_SYSTEM_OPTIONS -- discontinued JEDIT_APPLE_PROPERTIES; static default Dactors.corePoolSize=4 for more reproducible concurrency, independently of number of cores;

auto_flush: higher frequency;

uniform raw_dump for input/output fifos on Cygwin;

more robust fifo rendezvous: Cygwin 1.7 does not really block as expected;

Isabelle_Process: separate input fifo for commands (still using the old tty protocol); some partial workarounds for Cygwin;

tuned comments;

merged

added Lars Noschinski to isatest report

merged

discontinued separation of `define` and `declare_const`

unravelled target initialization code

added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)

added scanning of if-then-else expressions

merged

added support for partial quotient types; previously Nitpick was unsound for these