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