src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
changeset 36491 6769f8eacaac
parent 36486 c2d7e2dff59e
child 36496 8b2dc9b4bf4c
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Apr 28 14:19:26 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Apr 28 15:34:55 2010 +0200
@@ -6,6 +6,7 @@
 
 signature SLEDGEHAMMER_UTIL =
 sig
+  val is_new_spass_version : bool
   val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c
   val plural_s : int -> string
   val serial_commas : string -> string list -> string list
@@ -22,6 +23,18 @@
 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
 struct
 
+val is_new_spass_version =
+  case getenv "SPASS_VERSION" of
+    "" => case getenv "SPASS_HOME" of
+            "" => false
+          | s =>
+            (* Hack: Preliminary versions of the SPASS 3.7 package don't set
+               "SPASS_VERSION". *)
+            String.isSubstring "/spass-3.7/" s
+  | s => case s |> space_explode "." |> map Int.fromString of
+           SOME m :: SOME n :: _ => m > 3 orelse (m = 3 andalso n >= 5)
+         | _ => false
+
 fun pairf f g x = (f x, g x)
 
 fun plural_s n = if n = 1 then "" else "s"