Stream: Beginner Questions

Topic: Using LaTeXsugar

view this post on Zulip Gergely Buday (Nov 20 2020 at 11:44):

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?

view this post on Zulip Mathias Fleury (Nov 20 2020 at 11:49):

How about importing HOL-Library.OptionalSugar, that theory is listed in the ROOT file?

view this post on Zulip Mathias Fleury (Nov 20 2020 at 11:50):

Otherwise, you have to rebuild HOL-Library, but Isabelle will do that on its own on the next restart

Last updated: Oct 29 2025 at 04:28 UTC