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

tuned;

tuned;

clarified messages depending on options; misc tuning and simplification;

simplified "sos" method;

tuned signature; tuned whitespace;

tuned spelling; tuned whitespace;

add Linear Temporal Logic on Streams

move Code_Test to HOL/Library; add corresponding entries in NEWS and CONTRIBUTORS

proper bibliography;

more antiquotations;

more bibtex entries; more antiquotations;

more antiquotations;

tuned whitespace;

more antiquotations;

clarified whitespace;

more cartouches;

more cartouches;

more cartouches;

merged

more cartouches; more antiquotations;

more cartouches; more antiquotations;

more symbols;

more cartouches;

added update_cartouches tool;

removed pointless regexp flags;

fix document generation for HOL-Probability

move Stream theory from Datatype_Examples to Library

add Giry monad

tuned

improved spelling of formal INCOMPATIBILITY in historic versions (!) -- to avoid ad-hoc word completion multiply such lapses;

merged

tuned spaces

avoid creating needless skolemization steps for SPASS

get rid of 'individual' type in DFG proofs

slightly nicer names

strengthened 'moura' method

improved unskolemization of SPASS problems

more total parser;

more defensive error handling -- token marker must not crash;

merged

documentation of @{cite} and cite_macro;

completion for bibtex entries;

more accurate item name, depending on kind; tuned;

back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;

tuned signature;

add measure space for (coinductive) streams

add type for probability mass functions, i.e. discrete probability distribution

refactor 'map_sel_thms' and 'set_sel_thms'

rename 'xtor_rel_thms' to 'xtor_rels'

rename 'xtor_set_thmss' to 'xtor_setss'

rename 'xtor_map_thms' to 'xtor_maps'

rename one of the two 'rel_eq_thms' to 'rel_code_thms'

rename 'xtor_co_rec_transfer_thms' to 'xtor_co_rec_transfers'

rename 'dtor_set_induct_thms' to 'dtor_set_inducts'

rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct'

rename 'xtor_co_rec_o_map_thms' to 'xtor_co_rec_o_maps'

add 'set_inducts' to 'fp_sugar'

add 'common_set_inducts' to 'fp_sugar'

add 'rel_co_inducts' to 'fp_sugar'

add 'common_rel_co_induct' to 'fp_sugar'

add 'co_rec_transfers' to 'fp_sugar'

add 'co_rec_disc_iffs' to 'fp_sugar'

add 'disc_transfers' to 'fp_sugar'

add 'case_transfers' to 'fp_sugar'

add 'ctr_transfers' to 'fp_sugar'

add 'set_cases' to 'fp_sugar'

add 'set_intros' to 'fp_sugar'

add 'set_sels' to 'fp_sugar'

add 'set_thms' to 'fp_sugar'

add 'rel_cases' to 'fp_sugar'

add 'rel_intros' to 'fp_sugar'

add 'rel_sels' to 'fp_sugar'

add 'map_sels' to 'fp_sugar'

add 'map_disc_iffs' to 'fp_sugar'

code preprocessor tracing also for function transformers

basic support for fully static evaluator generation without dynamic compiler invocation

split dynamic from static context

more refs;

prefer @{cite} antiquotation;

prefer @{cite} antiquotation;

prefer @{cite} antiquotation;

prefer @{cite} antiquotation;

NEWS;

more explicit syntax, to avoid misunderstanding of foo-bar as 3 separate arguments;

clarified modules;

clarified modules;

clarified modules;

clarified modules;

citation tooltip/hyperlink based on open buffers with .bib files;

bibtex support in ML: document antiquotation @{cite} with markup;

maintain Document_Model.bibtex_entries; clarified Chunk predicates;

more advanced NEWS tree structure and folding;

merged;

NEWS;

tuned output;

proper treatment of @comment (amending 402a8e8107a7);

mark hard tabs as single chunks, as required by jEdit (see 0fd2bf8eaa9f);

more total chunk_line: recovery via ignored_line;

more explicit comments;

clarified nesting of delimiters; tuned;

fields are case-insensitive;

clarified nesting of delimiters;

more explicit chunk name;

clarified Chunk -- avoid ooddities;

support for bibtex token markup; more robust ML token marker: no_context; tuned signature;

more explicit item kind; clarified recover_delimited: skip to next @; support for line context parsing; tuned signature;

strict spaces for item_start: despite actual bibtex syntax, but in accordance to bibtex modes in Emacs and jEdit;

SideKick parser for bibtex entries; tuned signature;

more buffer.isEditable checks;

context menu for bibtex entries;