Stream: General

Topic: Importing from HOL

Gergely Buday (Jun 16 2026 at 14:42):

I am to tweak a file in the src/HOL directory. I copied it into my repository and gave an extended name, updated the theory name accordingly. Now the imports declaration does not work, the system looks for the files in the current directory, not in the HOL session. How can I make this work? My ROOT file is

session My_Spec = HOL +
  theories
      SpecTheory_MYVERSION

Is it a problem that the imported files are not present in the HOL session's ROOT file?

Kevin Kappelmann (Jun 16 2026 at 15:03):

You have to add the session qualifier HOL.
E.g. imports List becomes imports HOL.List

Gergely Buday (Jun 16 2026 at 15:33):

Follow-up: this line is not parsed:

 "card_order r ⟹ ( |A1| +c cone) ^c r = |Func UNIV (Inl ` A1 ∪ {Inr ()})|"

due to the vertical bar syntax for set cardinality. But I do import

HOL.BNF_Cardinal_Arithmetic

What do I miss compared to the original file?

Gergely Buday (Jun 16 2026 at 15:45):

Somehow the cardinal arithmetic notation does not propagate to my file.

Kevin Kappelmann (Jun 17 2026 at 07:54):

If it works in the original file and you haven't changed anything besides adding HOL. to the imports, it should work.

Mathias Fleury (Jun 17 2026 at 17:20):

+c is not exposed by default:

unbundle cardinal_syntax
lemma "card_order r ⟹ ( |A1| +c cone) ^c r = |Func UNIV (Inl ` A1 ∪ {Inr ()})|"
  sorry
unbundle no cardinal_syntax

Last updated: Jul 02 2026 at 14:06 UTC