generate lemma take_below, declare chain_take [simp]

switch to polyml-svn;

basic simplification of external_prover signature;

tuned;

renamed type_has_empty_sort to type_has_topsort -- {} is the full universal sort;
metis: type_has_topsort leads to tactic failure (with warning), like other metis failures;

point to http://hginit.com/

Simplified a couple of proofs and corrected a comment

lemmas set_map_of_compr, map_of_inject_set

merged

merged