[isabelle-dev] sledgehammer

[Mamoun FILALI-AMINE]

Hello (again, sorry my last message was not terminated),


I use the snapshot:
Unofficial version of Isabelle/HOL (Isabelle repository snapshot 
94b74365ceb9 (23-Mar-2009))
See also http://isabelle.in.tum.de/repos/isabelle/log/94b74365ceb9
(with polyml-5.2.1)

I have the following problem with the isabelle command sledgehammer:
Sledgehammer: external prover "remote_vampire" for subgoal 1:
finite {t?nat. t < (t'?nat) ? t mod b_period (b?'buffer) = deadline 
(owner b) mod b_period b}
Error: Bad executable: $ISABELLE_HOME/contrib/SystemOnTPTP/remote (I 
have an intel mac)

(by the way :
while if I execute: $ISABELLE_HOME/contrib/SystemOnTPTP/remote
Missing problem file at /usr/local/Isabelle/contrib/SystemOnTPTP/remote 
line 70
)

Has any one encountered these installation problems?

thanks

Mamoun