more flexibile font size via CSS <style> instead of old <font> element; preformatted text;

tuned;

control tooltip font via Swing HTML, with tooltip-font-size property;

added HTML.encode (in Scala), similar to HTML.output in ML;

one extra space to accomodate symbolic indentifiers etc.;

replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information; ML_Context.eval/expression expect explicit ML_Lex source, which allows surrounding further text without loosing position information; fall back on ML_Context.eval_text if there is no position or no surrounding text; proper Args.name_source_position for method "tactic" and "raw_tactic"; tuned;

more detailed token markup, including command kind as sub_kind; type-safe access to Command.HighlightInfo;

tuned;

separate markup for ML delimiters;

less pschedelic token markup;

simplified command/keyword markup;

markup non-identifier keyword as operator;

Isabelle_Process: do not enforce future_terminal_proof by default -- no error propagation yet;

more basic default behaviour of ENTER, HOME, END;

tuned messages;

do not highlight ignored command spans; tuned;

more explicit handling of document;

explicit markup for forked goals, as indicated by Goal.fork; accumulate pending forks within command state and hilight accordingly; Isabelle_Process: enforce future_terminal_proof, which gives some impression of non-linear/parallel checking;

avoid :\ which is not tail-recursive and tends to overflow the tiny JVM stack, which is not resizable at runtime;

define_state/new_state: provide state immediately, which is now lazy; more careful document editing: single execution future forces all entries, synchronous cancelation after update;

force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling; recovered some similarity to sequential version;

future result: retain plain Interrupt for vacuous group exceptions;

remove two examples, now that the definition of "fst" and "snd" has changed

merged

Got rid of a warning about duplicate rewrite rules.

accumulate only local results -- no proper history support yet;

avoid deprecated Iterator.fromArray;

more compiler warnings;

eliminated hard tabs;

assume given SCALA_HOME, e.g. from component settings or external setup;

merged

merged

make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work

Nitpick: show "..." in datatype values (e.g., [{0::nat, ...}]), since these are really equivalence classes

make Nitpick "show_all" option behave less surprisingly

merged

avoid reference to thm PairE

more coherent theory structure; tuned headings

made SML/NJ quite happy;

reuse main view.font from jEdit;

deleted some old fonts;

also set font for printing, which actually works out of the box;

lib/Tools/makeall does not hardiwre logics;

discontinued Sun/Solaris tests;

some updates for release;

merged

added function update examples and set examples

updated SMT certificates

sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks)

merged

renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")

made script executable

use Z3's builtin support for div and mod

moved SMT into the HOL image

slightly odd workaround to ignore markup that is typically displaced;

substantial performance improvement by avoiding "re-ified" execution structure via future dependencies, instead use singleton execution (dummy future) that forces lazy state updates bottom-up; tuned;

further formal thread-safety (follow-up to 88300168baf8) -- in practice there is only a single Isar toplevel loop, but this is not enforced;

renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;

renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;

misc updates for release;

constant Rat.normalize needs to be qualified;

merged

merged

dropped legacy theorem bindings

dropped legacy theorem bindings

dropped legacy theorem bindings

dropped legacy theorem bindings

dropped legacy theorem bindings

normalized references to constant "split"

Revise locale test theory layout.

Merge mixins of distinct interpretations with same base.

indicate prospective properties;

clarified auto_update vs. update; tuned;

more reactive message handling, notably for follow_caret mode; misc tuning and clarification;

Command.toString: include id for debugging; Command.consume: explicit forward, avoid dependency on Session and side-effect on event bus; State.+ without side-effect on event bus; Session.commands_changed: delayed command changes (outside of Swing thread), also subsumes former Session.results; Document_View: tuned commands_changed handling and caret listening; Document_View.selected_command: proper function, not event handler state; Output_Dockable: directly act upon commands_changed, not caret events (via former Session.results);

merged

refer to polyml-5.3.0-old for ppc-darwin;

try logical and theory abstraction before full abstraction (avoids warnings of linarith)

updated SMT certificates

hide constants and types introduced by SMT, simplified SMT patterns syntax, added examples for SMT patterns

more convenient order of code equations

misc updates for release;

eliminated obsolete priority message from Isabelle_Process protocol;

moved ML files where they are actually used; more precise dependencies;

renamed HOLCF/Library/ROOT.ML to HOLCF/Library/HOLCF_Library_ROOT.ML to avoid accidental uses of this ML file via the load path -- see also d7711be8c3a9 (obsolete) and ccae4ecd67f4;

eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML;

eliminated various catch-all exception patterns, guessing at the concrete exeptions that are intended here;

tuned -- avoid catch-all exception pattern;

updated generated files;

merged

merged

Typo fixed.

move HOLCF/Sum_Cpo.thy to HOLCF/Library

move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path

move unused pattern match syntax stuff into HOLCF/ex

rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed

more lemmas

induction and case rules

Store registrations in efficient data structure.

Avoid recomputation of registration instance for lookup.

Consistently use equality for registration lookup.

Cleaner implementation of sublocale command.

Reapply mixin patch: base for performance improvements.

merged

declare a few more cont2cont rules

HOLCF no longer redefines 'consts' command

for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run

simplify fixrec continuity tactic

used sledgehammer[isar_proof] to replace slow metis call

Typo fixed.

Typo fixed.

Minor proof tuning.