--- a/src/HOL/Tools/res_atp.ML Sat Nov 11 21:13:12 2006 +0100
+++ b/src/HOL/Tools/res_atp.ML Sat Nov 11 23:58:46 2006 +0100
@@ -51,6 +51,7 @@
val rm_simpset : unit -> unit
val rm_atpset : unit -> unit
val rm_clasimp : unit -> unit
+ val is_fol_thms : thm list -> bool
end;
structure ResAtp =
@@ -304,6 +305,8 @@
fun problem_logic_goals subgoals = problem_logic_goals_aux subgoals (FOL,[]);
+fun is_fol_thms ths = ((fst(logic_of_clauses (map prop_of ths) (FOL,[]))) = FOL);
+
(***************************************************************)
(* Retrieving and filtering lemmas *)
(***************************************************************)