--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 30 16:07:45 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 30 16:07:46 2011 +0200
@@ -74,6 +74,9 @@
val is_built_in_tptp_symbol : string -> bool
val is_tptp_variable : string -> bool
val is_tptp_user_symbol : string -> bool
+ val atype_of_types : (string * string) ho_type
+ val bool_atype : (string * string) ho_type
+ val individual_atype : (string * string) ho_type
val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
val mk_aconn :
connective -> ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula