Stream: Beginner Questions

Topic: theory error


view this post on Zulip 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

view this post on Zulip 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: Mar 29 2024 at 08:18 UTC