An old theory of mine uses the LaTeXsugar theory. It _would_ use:
*** Cannot load theory "HOL-Library.LaTeXsugar"
Should I rebuild the HOL-Library if I include LaTeXsugar in the HOL-Library section of HOL's ROOT file?
How about importing HOL-Library.OptionalSugar
, that theory is listed in the ROOT file?
Otherwise, you have to rebuild HOL-Library, but Isabelle will do that on its own on the next restart
Last updated: Dec 07 2024 at 16:22 UTC