Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
Also added function "repeat_RS" to the signature.
use "../settings.ML";
no_document use_thy "While_Combinator";
use_thy "simp";
use_thy "WFrec";
use_thy "Partial";