Re: [isabelle] Trying to rename Lattices.thy

On 24.06.2012 14:36, Gottfried Barrow wrote:
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.

Loading the HOL theories starting from Pure in jEdit can be done, but it is not straight-forward. Files need to be opened in a specific order (and/or you need a lot of reloading files), as jEdit does not yet handle the definition of new commands very well.

  -- Lars

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