src/HOL/Tools/ATP/system_on_tptp.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/system_on_tptp.ML	Fri Mar 12 23:30:35 2021 +0100
@@ -0,0 +1,20 @@
+(*  Title:      HOL/Tools/ATP/system_on_tptp.ML
+    Author:     Makarius
+
+Support for remote ATPs via SystemOnTPTP.
+*)
+
+signature SYSTEM_ON_TPTP =
+sig
+  val get_url: unit -> string
+  val list_systems: unit -> string list
+end
+
+structure SystemOnTPTP: SYSTEM_ON_TPTP =
+struct
+
+fun get_url () = Options.default_string \<^system_option>\<open>SystemOnTPTP\<close>
+
+fun list_systems () = get_url () |> \<^scala_thread>\<open>SystemOnTPTP.list_systems\<close> |> split_lines
+
+end