Re: [isabelle] Trying to rename Lattices.thy
On Mon, 25 Jun 2012, Florian Haftmann wrote:
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.
AFAIK this restriction does not hold any longer.
* Prover IDE (PIDE) improvements:
- support for user-defined Isar commands within the running session
For most practical situation you just load the theory that you have in
mind, and it should all work as expected. (There might still be an odd
boundary case where one final "File / Reload" in jEdit is needed after all
new commands have been defined via loading the imports.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and