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
This archive was generated by a fusion of
Pipermail (Mailman edition) and