yuuuu (Apr 23 2022 at 03:12): yuuuu (Apr 23 2022 at 03:12):I am trying to open the theory "Complete_Lattices", but an error is occurred which says "Cannot update finished theory "HOL.Complete_Lattices". Snipaste_2022-04-23_11-10-52.jpg
Lukas Stevens (Apr 25 2022 at 08:25):This is to be expected since HOL.Complete_Lattices is part of the pre-built HOL image. Since you are building on the image, theories contained therein can't be changed any more. You can base your (interactive) session on Pure instead. Then this message will disappear. This can be done by launching Isabelle with isabelle jedit -l Pure.
Last updated: Dec 21 2024 at 16:20 UTC