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;