enable variant of transfer method that proves an implication instead of an equivalence

moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator

merged

NEWS for transfer, lifting, and quotient

new example theory for transfer package

some builtin session timing;

move alternative definition lemmas into Lifting.thy; simplify proof of Quotient_compose

tuned proofs

add transfer rule for List.set

remove duplicate of lemma id_transfer

added covariant relator set_rel, with transfer rules for set operations

renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator

tried to make SML/NJ happy

tuned "max_relevant" defaults for SMT solvers based on Judgment Day

prepend PWD to relative paths

reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures

swap out Satallax, pull in E-SInE again -- it's not clear yet how useful Satallax is after proof reconstruction, whereas E-SInE performed surprisingly well on latest evaluations

new transfer package rules and lifting setup for lists

strengthen rule list_all2_induct

more standard Theory_Data setup; keep meta-comments within the history;

merged

add transfer rule for nat_case

uniform naming scheme for transfer rules

rename 'correspondence' method to 'transfer_prover'

hide the invariant constant for relators: invariant_commute infrastracture

improved interleaving of start_execution vs. cancel_execution of the next update;

tuned proofs;

always revisit nodes independently of "required" flag, which may change during editing -- avoid "bloodbath effect" when changing perspective while loading;

tuned;

simplified internal actor protocol;