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

adapt occurrences of renamed Nitpick functions

document the non-legacy interfaces

local versions of Nitpick.register_xxx functions

parse_spans: somewhat faster low-level implementation;

proper context for Syntax.parse_token;

prefer Context_Position.report where a proper context is available -- notably for "inner" entities;

explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);

fixed odd runtime type error, which appears to have escaped the scala-2.8.0.final compiler;

YXML.parse: refrain from interning, let XML.Cache do it (partially);

cache_string: store trimmed string value;

simple_dialog: allow scala.swing.Component as well;

simplified some Markup;

simplified type XML.Tree: embed Markup directly, avoid slightly odd triple; XML.cache_tree: actually store XML.Text as well; added Isabelle_Process.Result.properties;

more robust treatment of Markup.token;

simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;

concentrate structural document notions in document.scala; tuned;

maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);

tuned;

more explicit model of pending text edits;

more explicit treatment of Swing thread context; Document_Model.snapshot: require Swing thread;

replaced individual Document_Model history by all-inclusive one in Session; Document_Model: provide thy_name externally, i.e. by central Isabelle plugin; tuned;

misc tuning and clarification;