Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Sledgehammer in FOL

view this post on Zulip Email Gateway (Aug 18 2022 at 12:30):

From: "julien@RadboudUniversity" <julien@cs.ru.nl>
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@cs.ru.nl --- www.cs.ru.nl/~julien/
Phone: +31 24 36 52104 --- Fax: +31 24 365 2728

Last updated: Nov 21 2024 at 12:39 UTC