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;