Re: [isabelle] Trying to rename Lattices.thy



On 6/24/2012 6:30 AM, 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.

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

Tjark,

One of the main purposes is to open up HOL distribution sources for reference purposes while I'm doing my own HOL theories. And it's nice to do that in jEdit so that I can copy and paste original lemmas, etc., rename them, and experiment with them in the same file.

Renaming Lattices.thy to Li12H05lat.thy works, so that's good enough.

However, when renaming other theories, if I have a problem, I'll use Pure as the logic to make sure that the problem is not a conflict due to having HOL loaded as the logic.

Regards,
GB






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