[isabelle-dev] Isabelle/jEdit: non-trivial theory merge
makarius at sketis.net
Thu Mar 15 23:09:25 CET 2012
On Mon, 12 Mar 2012, Makarius wrote:
> There is still no proper support for redefining Isar commands in the
> running session. So I would say the above is the normal consequence of
> redefining 'function' in one theory while another one already reparses
> an older version of it. Thus the resulting transaction is from a
> different theory (different version with the same name).
> Isabelle/8f3bb485f628 tries to make it a bit less erratic: commands are
> always parsed dynamically.
Some more substantial refinements are in Isabelle/9ff441f295c2. This
means sessions like HOL or ZF should now be editable with Isabelle/jEdit
without worries. (A little bit of fine-tuning is still coming.)
More information about the isabelle-dev