Variable.names_of; tuned;

more details on Isabelle symbols;

theory data example;

basic setup for ML examples: tag "mlex";

tuned signature;

formal markup of type aliases; updated/tuned/clarified contexts; misc tuning and clarification;

make underscores visually appear as such, although TeX-nically they are just rules (e.g. cannot be searched);

Netbeans Library "Scala-compiler";

union is an abbreviation for sup.

merged

Eliminated is_open option of Rule_Cases.make_nested/make_common; use Rule_Cases.internalize_params to rename parameters instead.

Adapted to changes in induct method.

Adapted to changes in setup of induct method.

Expand proofs of induct_atomize'/rulify'.

Changed case names of converse_rtranclp_induct.

Injectivity / distinctness theorems are now used to simplify induction rules.

same_append_eq / append_same_eq are now used for simplifying induction rules.

Tuned some proofs; nicer case names for some of the induction / cases rules.

Added setup for simplification of equality constraints in induction rules.

Added infrastructure for simplifying equality constraints. Option (no_simp) restores old behaviour of induct method.

spurious proof failure

merged

merged

dropped unused binding

dedicated conversions to and from Int

printing of cases

tuned for products vs. tupled functions

added Scala setup

allow individual printing of numerals during code serialization

reorder Quickcheck and Nitpick, so that Quickcheck gets loaded first and Auto-Quickcheck runs first (since it takes less time)

adjusted to changes in code equation administration

explicit abstract type of code certificates

corrected error messages; tuned

function transformer preprocessor applies to both code generators

merged

code certificates as integral part of code generation

import of antiquote_setup not necessary

merged

being more accurate wrt. list syntax

deactivate pretty code test for Scala -- no proper setup yet

some syntax setup for Scala

added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;

merged

Parsing errors during proof reconstruction now give rise to an intelligible error message.

rebuilt from fresh copy of Bitstream Vera, for improved quality of regular text glyphs; misc cleanup of mathematical glyphs, with bold version synthesized by fontforge;

tuned initial properties/perspective;

provide JEDIT_SETTINGS via settings; provide default perspective; tuned default properties;

updated version and dependencies;

recovered subscript (cf. ded5b770ec1c);

formal antiquotations for ML snippets; no "open" unsynchronized references

clarified terminology;

merged

added code certificates

tuned code equations

Matrices form a semiring with 0

incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);

ignore some src/Tools/jEdit stuff;

merged with converted/relocated copy of http://isabelle.in.tum.de/repos/isabelle-jedit/rev/93d884afa74b

more timing;

more tobust treatment of Document.current_state; some timing;

new unparsed span for text right after existing command; tuned;

Outer_Lex.is_ignored;

simplified Text_Edit;

eliminated strange mutable var commands; removed_commands: refer to old commands; misc tuning;

updated header;

eliminated obsolete isabelle.proofdocument.Token;

do not override Command.hashCode -- which was inconsistent with eq anyway; unparsed: no id, commands observe pointer equality; actually invoke edit_commands; more correct doc_edits; tuned;

renamed Command.content to source; reorganization of document parsing, using command spans etc. -- initial setup;

further tuning of command_start;

refrain from poking blink rate -- might get stuck in invisible state;

eliminated Command.stop, which tends to case duplicate traversal of commands;

iterators for ranges of commands/starts -- avoid extra array per document; try/finally for saved_color; misc tuning;

tuned document changes;

misc tuning and clarification of Document/Change;

adhoc reset of blink rate; bind "console" instance;

provide global "Isabelle" within interpreter loop -- using import instead of val avoids pontential conflicts with later import isabelle.jedit._;

redirect scala.Console output during interpretation; misc tuning;

bind "session"; added printInfoMessage; added stop -- re-inits the interpreter;

export isabelle_system, e.g. for use via "session" in Isabelle/Scala interpreter;

removed unused var plugin;

pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space; reduced predefined values, which take time and are static anyway;

provide some bindings of jEdit values; plain color for input;

more precise prompt etc.;

define scala.home, for more robust startup of Scala tools, notably the compiler;

added jEdit Console and Scala compiler;

some attempts at Scala console plugin;

more precise treatment of document/state assigment;

more precise notion of bad messages;

use Text_Edit provided by Isabelle;

result.is_ready is not bad;

singleton status messages, with more precise patterns -- report bad messages;

back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states; recent_document: require finished state assignment; explicitly typed Session.lookup_command;

slightly more uniform/robust handling of visible document; uniform changed_delay for view updates; misc tuning;

recovered explicit Changed.id (copy of future document) -- avoids premature joining of result; Change.ancestors: frugal iterator;

more explicit treatment of command/document state; misc tuning and clarification;

removed unused document_change bus;

tuned;

tuned;

misc tuning;

tuned Change: eliminated redundant copy of document id;

eliminated redundant session documents database; tuned;

use isabelle.Future; tuned;

renamed current_document to recent_document (might be a bit older than current_change); Change: explicit future value of Document.Change instead of implicit lookup in Session database; Document_Model: apply Document.text_edits here (as future);

renamed Proof_Document to Document;

tuned dialog;

improved dialog;

basic setup for synchronous / modal (!) prover startup;

tuned signature;

register Proof_Document instances as session entities -- handle Markup.EDIT messages locally;

tuned signature of isabelle.Position;

maintain generic session entities -- cover commands, states, etc. (but not yet documents);

unified Command and Command_State, eliminated separate Accumulator; Command.finish_static: idempotent transition from static to dynamic mode, taking snapshot of final state (which will never change later);

removed experimental history panel;

more explicit modeling of Command and Command_State as Session.Entity; misc tuning;

updated;

tuned;

tuned caret_listener/selected_command;

misc tuning;

eliminated global Session.document_0 -- did not work due to hardwired id; more precise Session.begin_document, avoid race on var prover; replaced slightly odd Session.document_versions by Sassion.documents table (cf. src/Pure/Isar/isar_document.ML); simplified edit_document in ML: initial empty command is identified by ""; misc tuning;

tuned;