dropped dead code

moved Record.thy from session Plain to Main; avoid variable name acc

group record-related ML files

Class.declare -> Class.const

named target is optional; explicit Name_Target.reinit

named target is optional

Named_Target.init: empty string represents theory target

Named_Target.theory_init

simplified code

tuned

tuned

merged

tuned whitespace

tuned internal structure

remove reinit operation alltogether

avoid arcane Local_Theory.reinit entirely

more convenient split of class modules: class and class_declaration

tuned

stripped signature

explicit accessed to structure Class_Target

tuned lowercase

moved Document.text_edits to Thy_Syntax;

tuned;

added Isabelle_Process.input_bytes, which avoids the somewhat slow Standard_System.string_bytes (just in case someone wants to stream raw data at 250MB/s);

do not buffer fifo streams here -- done in Isabelle_Process; removed misleading comments -- blocking on open is not reliable on non-standard systems (Cygwin);

explicit Document.State value, instead of individual state variables in Session, Command, Document; Session.snapshot: pure value based on Document.State; Document.edit_texts: no treatment of state assignment here;

edit_document: more precise status position;

added get_after convenience;

more basic notion of unparsed input;

simplified/clarified Change: transition prev --edits--> result, based on futures; Session.history: plain List instead of somewhat indirect Change.ancestors; tuned;

moved snapshot to Session (cf. 96b22dfeb56a);

Change: eliminated id, which is merely the resulting document id and is only required in joined state anyway; Document.edit_text: create new document id here;

clarified "state" (accumulated data) vs. "exec" (execution that produces data); generic type Document.id (ML) / Document.ID;

misc tuning and simplification;

specific command state;

specific Session.Commands_Changed;

consider snapshot as service of Session, not Document.Change;

tuned scope;

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