what does Isabelle error Cannot update finished theory "HOL.Finite_Set" mean?

Question

I am trying to use the theory Finite_Set.thy but when I import it

imports "$ISABELLE_HOME/SRC/HOL/Finite_Set"

the theory I am working on is not parsed. When I open the theory itself, I receive the following error:

Cannot update finished theory "HOL.Finite_Set"

I am not sure what this means (or if it is related) or what I can do about it.

Answer 1

A similar question has already been asked on the Isabelle mailing-list

Finite_Set is part of HOL and cannot be edited (and you cannot click on it to open definitions and so on). You should import Main (aka HOL.Main) instead of only Finite_Set.

If you really want to import only Finite_Set, you should import via HOL.Finite_Set, not by giving a full path.

However, this should not be the cause of your problem.