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
