eliminated dead code;

inner syntax positions for string literals;

less confusion subexpression markup;

pass positions for named targets, for formal links in the document model;

simplified Runtime.exn_messages: always print detailed version of low-level exeptions, which should not occur in regular user errors anyway;

more detailed exception_trace: in Poly/ML 5.4.x intermediate handlers reset the trace (cf. Poly/ML SVN 1110);

merged

setting up exhaustive generators which are used for the smart generators

add Code_Real_Approx_By_Float

merged

remove lemma float_remove_real_numeral, which duplicated Float.float_number_of

remove unnecessary number-representation-specific rules from metis calls; speed up another proof

avoid confusing selector output

remove unsound line in Nitpick's "rat" setup

tuned proofs;

merged

removed some old-style semicolons

index markup elements for more efficient cumulate/select operations;

tuned;

tuned markup -- prefer user-perspective;

tuned specifications and proofs;

more precise type;

refined Markup_Tree implementation: stacked markup within each entry; tuned;

tuned signature; express select in terms of cumulate;

tuned signature;

merged

merged

abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite; add tests for abel_cancel simprocs