Is there a good/stable way to load ML files from another session (e.g. the AFP)?
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.
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.
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
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.
Kevin Kappelmann has marked this topic as resolved.
Last updated: Dec 07 2023 at 16:21 UTC