Kevin Kappelmann (Dec 02 2021 at 16:45): Kevin Kappelmann (Dec 02 2021 at 16:45):Is there a good/stable way to load ML files from another session (e.g. the AFP)?
Manuel Eberl (Dec 02 2021 at 16:48):The only way I can think of is: make a theory file that includes it with ML_file. In the respective session. Then import that theory file in your session.
Kevin Kappelmann (Dec 02 2021 at 17:13):I think I sadly can't do that: the ML file I want to load expects the existence of an ML structure of a certain name that I need to create in my session.
Kevin Kappelmann (Dec 02 2021 at 17:16):To provide some background: I wanted to have my own auto2 instance but it loads a bunch of ML files that expect one custom ML structure created in the file auto2_HOL.ML in the AFP entry: https://www.isa-afp.org/browser_info/current/AFP/Auto2_HOL/Auto2_HOL.html
I do not know how I would load the next file util_logic.ML that depends on that structure once I created my replacement for auto2_HOL.ML.
Kevin Kappelmann (Dec 03 2021 at 22:04):The "solution" was that I decided to bite the bullet and do the right thing: fix the setup of the AFP entry that I wanted to use.
Notification Bot (Dec 03 2021 at 22:04):Kevin Kappelmann has marked this topic as resolved.
Last updated: Dec 21 2024 at 16:20 UTC