more explicit keyword1/keyword2 markup -- avoid potential conflict with input token markup produced by Token_Marker;

updated checksum, which appears to have changed accidentally;

updated to exec_process-1.0.2;

search bash via PATH as usual (this is no longer restricted to Cygwin with its known file-system layout);

discontinued futile attempt to hardwire build options into the image, sequential mode is enabled more robustly at runtime (cf. 3b0a60eee56e);

Mirabelle appears to work better in single-threaded mode;

generalized types

tuned termination proof

adapted examples to new names

renamed coinduction principles to have "dtor" in the name

renamed "set_incl" etc. to have "ctor" or "dtor" in the name

renamed low-level "map_unique" to have "ctor" or "dtor" in the name

renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name

renamed "map_simps" to "{c,d}tor_maps"

took out accidentally submitted "tracing" calls

fixed bug in "fold" tactic with nested products (beyond the sum of product corresponding to constructors)

simplified fact policies

generate "rel_as_srel" and "rel_flip" properties

started work on generation of "rel" theorems

make smlnj happy

more strict typscheme_equiv check: must fix variables of more specific type; dropped dead code; tuned order

cache should not contain material from descendant theory

some PIDE NEWS from this summer;

tuned whitespace;

tuned;

tuned proofs;

report proper binding positions only -- avoid swamping document model with unspecific information;

accumulate under exec_id as well;