Email Gateway (Jul 17 2022 at 13:10): Email Gateway (Jul 17 2022 at 13:10):From: Adam Dingle <adam.dingle@mff.cuni.cz>
Hello -
I'd like to try using the auto2 prover in writing an Isabelle proof:
<https://github.com/bzhan/auto2>
It appears that it's not included in the standard Isabelle
distribution. So I cloned it to a local directory
(/home/adam/src/auto2). Now I'd like to install it so that I can use
the 'auto2' tactic in any proof that I write. Unfortunately I'm not
sure about how to proceed, even after studying the Isabelle System
Manual. As one attempt, I created a file ~/.isabelle/ROOTS with this
text:
/home/adam/src/auto2
Then at the top of my theory file I wrote
theory arith
imports Main "Auto2_HOL.Auto2_Main"
begin
...
I tried various variations of the 'imports' statement, but Isabelle
always reported
Bad theory import "Auto2_HOL.Auto2_Main"
I'm not even sure if I'm using the right approach. Should I instead
use the 'isabelle' command-line tool to register this library somehow?
Any advice would be appreciated. Thanks -
Adam
Email Gateway (Jul 17 2022 at 13:19):From: Kevin Kappelmann <kevin.kappelmann@tum.de>
Hi Adam,
auto2 is part of the AFP:
https://www.isa-afp.org/entries/Auto2_HOL.html
Please use that version. Instructions on how to use AFP entries can be
found here:
https://www.isa-afp.org/help/
Best wishes,
Kevin
Last updated: Apr 26 2024 at 08:19 UTC