[isabelle] Sledgehammer in FOL



Dear All,

is it possible to use sledgehammer in Isabelle/FOL ? I load FOL in ProofGeneral, and then I import FOL. But "metis" is then unknown. Am I doing something wrong ?

Thanks for your answer.

Best regards,

Julien

------------------------------------------------------------------------
Dr. Julien Schmaltz
Model Based System Development (MBSD)
Institute For Computing and Information Sciences
Radboud University  Nijmegen
The Netherlands
julien at cs.ru.nl   --- www.cs.ru.nl/~julien/
Phone: +31 24 36 52104  ---  Fax:   +31 24 365 2728
------------------------------------------------------------------------








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.