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};