Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] base session in ROOT file for AFP submission

view this post on Zulip Email Gateway (Oct 01 2024 at 17:11):

From: Angeliki Koutsoukou Argyraki <ak2110@cam.ac.uk>
Hi,
I'm in the process of submitting an AFP entry importing "HOL-Library.Library" "HOL-Real_Asymp.Real_Asymp"

What is the exact syntax to include this in the ROOT file?
What I've tried so far causes errors.

Thanks,
Angeliki

view this post on Zulip Email Gateway (Oct 03 2024 at 13:22):

From: Lawrence Paulson <lp15@cam.ac.uk>
Hi Angeliki,

You are allowed to import only one session in the initial "session" line, but can import further sessions under the “sessions" heading.

chapter AFP

session Catalan_Numbers = "HOL-Analysis" +
options [timeout = 600]
sessions
Landau_Symbols
"HOL-Real_Asymp"
theories
Catalan_Numbers
document_files
"root.tex"
"root.bib"

Larry

On 1 Oct 2024, at 18:11, Angeliki Koutsoukou Argyraki <ak2110@cam.ac.uk> wrote:

Hi,
I'm in the process of submitting an AFP entry importing "HOL-Library.Library" "HOL-Real_Asymp.Real_Asymp"

What is the exact syntax to include this in the ROOT file?
What I've tried so far causes errors.

Thanks,
Angeliki

Last updated: Jan 04 2025 at 20:18 UTC