src/HOL/Tools/res_atp.ML
changeset 21311 3556301c18cd
parent 21290 33b6bb5d6ab8
child 21373 18f519614978
     1.1 --- a/src/HOL/Tools/res_atp.ML	Sat Nov 11 21:13:12 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Sat Nov 11 23:58:46 2006 +0100
     1.3 @@ -51,6 +51,7 @@
     1.4    val rm_simpset : unit -> unit
     1.5    val rm_atpset : unit -> unit
     1.6    val rm_clasimp : unit -> unit
     1.7 +  val is_fol_thms : thm list -> bool
     1.8  end;
     1.9  
    1.10  structure ResAtp =
    1.11 @@ -304,6 +305,8 @@
    1.12      
    1.13  fun problem_logic_goals subgoals = problem_logic_goals_aux subgoals (FOL,[]);
    1.14  
    1.15 +fun is_fol_thms ths = ((fst(logic_of_clauses (map prop_of ths) (FOL,[]))) = FOL);
    1.16 +
    1.17  (***************************************************************)
    1.18  (* Retrieving and filtering lemmas                             *)
    1.19  (***************************************************************)