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.

See Isabelle2012/NEWS:

  * 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 MHonArc.