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: Feb 27 2024 at 08:17 UTC