Re: [isabelle] Trying to rename Lattices.thy

On Sun, 24 Jun 2012, Tjark Weber wrote:

On Sat, 2012-06-23 at 23:56 -0500, Gottfried Barrow wrote:
I'm trying to rename HOL/Lattices.thy so I can load it, experiment with
it, and mark it up, but it's picky about what it's name can be.

"Yea, don't do that."

Isabelle/HOL is based upon a complex bootstrapping process, with
intertwined setup of theories and proof tools. If you import Main, you
get a reasonably clean entry point. If you import anything below Main,
you may be exposed to the intricacies of this process.

Indeed. Importing anything apart from Main or Complex_Main means you investigate the way Isabelle/HOL is bootstrapped, so it is no good for applications, but sometimes helps to understand how things work.

If you are sure this is what you want, you can load Lattices.thy (and
other theories that are part of Isabelle/HOL) by choosing Pure as the
logic image for your session: e.g.,

 isabelle jedit -l Pure Isabelle2012/src/HOL/Lattices.thy

Yes, this is the official workaround to peek into parts of the Isabelle/HOL session, until the next big reform of the theory loader in connection with the interactive document model.

In rare cases one does have to rename such an intermediate theory, but then the obvious thing is to turn Lattices into Lattices1, say. This might require some other renaming nonetheless, as you have noticed already.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.