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

Best regards,
Tjark







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