author | paulson |
Thu, 17 May 2007 13:37:24 +0200 | |
changeset 22989 | 3bcbe6187027 |
parent 22988 | f6b8184f5b4a |
child 22990 | 775e9de3db48 |
--- a/src/HOL/Tools/res_atp.ML Thu May 17 08:53:57 2007 +0200 +++ b/src/HOL/Tools/res_atp.ML Thu May 17 13:37:24 2007 +0200 @@ -45,6 +45,9 @@ val rm_atpset : unit -> unit val rm_clasimp : unit -> unit val is_fol_thms : thm list -> bool + val tvar_classes_of_terms : term list -> string list + val tfree_classes_of_terms : term list -> string list + val type_consts_of_terms : theory -> term list -> string list end; structure ResAtp: RES_ATP =