tuned

reorganized examples

fixed slips

re-canibalised manual

slightly different command line for makedist_mercurial

put_thms: ContextPosition.set_visible false;

added type pp, which helps installing polymorphic pretty printers;

added str_of;

install_pp Future.T (polyml only);

report_token/parse_token: back to context-less version;

back to plain Position.report for regular references;

back to plain Position.report for regular references; ContextPosition.report_visible for decls; report_token/parse_token: back to context-less version;

promise global proofs;

renamed report to report_visible; tuned comments;

code example: back to individual ML commands, which are now thread-safe;

ContextPosition.report; parse_token/report_token: explicit context;

target update: invisible context position avoids duplication of reports etc.;

Context position visibility.

added context_position.ML;

more precise redundancy check

clarified dependencies between arith tools

separate HOL-Main image

polished code generator setup

added theory antiquotation

tuned comments;

handle _ should be avoided (spurious Interrupt will spoil the game);

added norm_export_morphism;

added exit_global, exit_result, exit_result_global; ProofContext.norm_export_morphism;

LocalTheory.exit_global;

HOL no longer depends on HOL-Plain;