tuned;

support for begin/end matching;

proper token kind;

added option jedit_structure_limit; tuned signature;

some structure matching, based on line token iterators;

support for structure matching; misc tuning;

tuned rendering;

back to alternative fold painter, despite f03a9c57760a -- gutter painter seems to have changed in the meantime;

tuned;

update_cartouches;

clarified tree root;

tuned spacing;

clarified verbatim line breaks, e.g. relevant for Implementation mldecls;

turn even into an abbreviation

update documentation for 'size_o_map'

rename 'size_o_map' to 'size_gen_o_map'

document 'size_gen'

generate 'size_gen' for datatypes

document 'map_o_corec'

generate 'map_o_corec' for (co)datatypes * * * document 'map_o_corec'

move documentation of 'rec_o_map'

move theorem 'rec_o_map' * * * move documentation of 'rec_o_map'

warn for not fully mutually (co)recursive types

add transfer rule for set_pmf

add tendsto_const and tendsto_ident_at as simp and intro rules

tuned spacing;

avoid odd ligatures;

more accurate approximation of AST;

tuned exposition of {* ... *};

more antiquotations; tuned spacing;

more antiquotations; tuned spacing;

register transfer rules from BNF and FP_Sugar

refactored

merged

back to formal comment (see 23a380cc45f4, 3094b0edd6b5);

repared document;

merged

official support for "tt" style variants, avoid fragile \verb in LaTeX; official document antiquotation @{verbatim};

removed dead code;

suppress special Poly/ML location inBasis (see $ML_SOURCES/mlsource/MLCompiler/STRUCT_VALS.ML);

tweaked

avoid unsafe simp rules

more standard declaration for presburger

augmented and tuned facts on even/odd and division

prefer generic elimination rules for even/odd over specialized unfold rules for nat

NEWS;

omit pointless nodes for proof commands etc.;

tuned signature and modules;

merged

NEWS;

more folds;

always apply precedingFoldLevels, avoid unclear shortcuts; updated Console.jar 5.1.4;

make double-sure that line context is present, e.g. relevant for last line after visible text;

clarified Line_Structure wrt. command span;

tuned signature;

tuned signature;

tuned signature;

more explicit Line_Nesting;

tuned comments;

support line context with depth; basic setup for "isabelle" fold handling; misc tuning;

proper type comparison (amending cd4439d8799c);

tuned;

tuned

standard elimination rule for even

tuned facts on even and power

restructured

even more cleanup

made SML/NJ happier

made SML/NJ happier

tuned whitespace

buffer_line_context via untyped access;

access class hierarchy; smash access to null;

legacy cleanup

more algebraic deductions for facts on even/odd

more algebraic deductions for facts on even/odd

purely algebraic characterization of even and odd

document 'sel_transfer'

generate 'sel_transfer' for (co)datatypes

add 'kind' to 'cr_sugar'

add 'fp_bnf' to 'bnf_sugar'

preserve the structure of 'set_intros' theorem in ML

preserve the structure of 'map_sel' theorem in ML

preserve the structure of 'set_sel' theorem in ML

Fixed bug in waldmeister skolemization

tuned signature;

tuned signature;

merged

tuned signature;

tuned signature;

obsolete;

module Interpretation is superseded by Plugin;

module Interpretation is superseded by Plugin;

module Interpretation is superseded by Plugin;

clarified load order; tuned signature;

Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;

support for indirections (defined entries), e.g. relevant for quickcheck and its sub-plugins;

support for named plugins for definitional packages;

relaxed class constraints for exp

tuned

special treatment of extensionality in minimizer

improved handling of extensionality in Isar proofs generated from LEO-II and Satallax

made SML/NJ happier

leftover from 3ccafeb9a1d1

some more facts on divisibility

generalized and consolidated some theorems concerning divisibility

eliminiated clone

more facts about abstract divisibility

specialized specification: avoid trivial instances

more foundational definition for predicate even

New example Bubblesort

formally completeted set of experimental static evaluation functions

merged

afford slightly bigger JVM stack (see also f7ba30a816b9);

prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within read-only directory (due to its bundled Cygwin and /tmp inside of it);

prefer Unix standard-conformant $TMPDIR over hard-wired /tmp;

proper @{cite} with bibtex entry (unchecked comment);

fix document generation in Code_Test

merged

eliminated some exotic combinators;

added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};