added String.isSubstring;

export is_finished; added thy_ord (based on update_time); begin_thy/register_thy: more precise handling of update_time;

Present.session_name;

tuned signature; tuned message;

thy_deps: ThyInfo.thy_ord, improved dir/unfold entry;

removed thy_ord (erratic due to multi-threading);

some cleaning up

theorem: apply hook last;

reset goal messages after goal update;

added hilite markup;

fixed type alias in signature;

added lemma

allow TVars during type inference

tidied the proofs

made smlnj happy;

new fun declaration