--- a/src/HOL/Tools/ATP/atp_systems.ML Mon Aug 29 13:50:47 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 30 14:12:55 2011 +0200
@@ -55,6 +55,7 @@
val get_atp : theory -> string -> atp_config
val supported_atps : theory -> string list
val is_atp_installed : theory -> string -> bool
+ val is_ho_atp: string -> bool
val refresh_systems_on_tptp : unit -> unit
val setup : theory -> theory
end;
@@ -499,6 +500,15 @@
forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
end
+fun is_ho_atp name =
+ let
+ val local_ho_atps = [leo2N, satallaxN]
+ val ho_atps = map (fn n => remote_prefix ^ n) local_ho_atps
+ in List.filter (fn n => n = name) ho_atps
+ |> List.null
+ |> not
+ end
+
fun refresh_systems_on_tptp () =
Synchronized.change systems (fn _ => get_systems ())