Re: [isabelle] Trying to rename Lattices.thy
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.
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and