1) have adjusted the swapping of the result type in add_datatype_i 2) have replaced map_nth_elem by Library.nth_map (there seems to be a clash with an existing nth_map somewhere - therefore the "Library")

tuned;

lthms_containing: not o valid_thms;

added fact_tac, some_fact_tac; retrieve_thms: support literal facts; tuned export interfaces;