lemma, equation between rtrancl and trancl

enter_thms: use theorem database of thy *after* attribute application;

tuned;

added subset, eq_set; tuned insert/remove: avoid garbage;

tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;

fixed HOL-Complex-Matrix target;

removed mkcontent from makedist

fix 'give up waiting message' (logs of running processes are not attached)

* Pure: get_thm interface expects datatype thmref; * More efficient treatment of intermediate theory checkpoints;

avoid identifier 'Name';

Theory.begin/end_theory;

clarify empty vs. pure browser info;

added pointer_eq;

thmref: Name vs. NameSelection; tuned;

refl_tac: avoid failure of unification, i.e. confusing trace msg; get_thm(s): Name;

print_theorems: proper use of PureThy.print_theorems_diff;

thmref: Name vs. NameSelection;

generalized type of inter; added substract; economize heap usage;

added previous;

added begin_theory, end_theory;

added certify_prop, cert_term, cert_prop;

datatype thmref = Name ... | NameSelection ...; added print_theorems_diff; tuned;

added member, option_ord;

OrdList.inter;

tuned;

improved treatment of intermediate checkpoints: actual copy instead of extend, purge after end; tuned;

added add_fixrec_i, add_fixpat_i; ThyParse obsolete; Sign.read_prop, Sign.cert_prop;

proper header;