Document.print_id;

consider command state as part of Snapshot, not Document;

represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);

Named_Target;

modernized specifications; tuned headers;

spelling;

merged

renamed Theory_Target to the more appropriate Named_Target

discontinue old implementation of `foundation`

moved instantiation target formally to class_target.ML

NEWS

merged

print fcomp combinator only monadic in connection with other monadic expressions

merged

merged

moved overloading target formally to overloading.ML

moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order

merged

whitespace tuning

remove overloading and instantiation from data slot

removed obsolete Toplevel.enter_proof_body;

standardized pretty printing of consts (e.g. see find_theorems, print_theory);

misc tuning and simplification;

simplified/unified command setup;

removed obsolete Proof.get_thmss_cmd (cf. Attrib.eval_thms);

prefer plain Attrib.eval_thmss -- also means the assert_forward of Proof.get_thmss_cmd is skipped, leading to uniform (albeit odd) behaviour concerning forward chaining; tuned;

prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;

tuned eval_thms (cf. note etc. in proof.ML);

use Pretty.enum convenience;

tuned whitespace;

more precise and more maintainable dependencies;

merged, resolving conflict in src/Pure/IsaMakefile concerning General/xml_data.ML;

* -> prod

added .ML extension

avoid old unnamed infix

avoid inclusion of Natural module in generated code

explicit ML extension

merged

separate initialisation for overloading and instantiation target

different foundations for different targets; simplified syntax handling of abbreviations

deleted duplicate lemma

Revert performance improvement of 8ed3a5fb4d25 since it breaks notes element declarations.

basic renumbering

avoiding redundant primes

separated type from term parameters

moved extra_tfrees check for mixfix syntax to Generic_Target

name and argument grouping tuning

whitespace tuning

added generic_target.ML

try to uniformly follow define/note/abbrev/declaration order as close as possible

split off structure Generic_Target into separate file

split off generic parts of target implementations into separate structure

restructured code for `declaration`

executable relation operations contributed by Tjark Weber

factored out foundation of `define` into separate function

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;