[isabelle-dev] [isabelle] Incompatibilities between releases

Tjark Weber tjark.weber at gmx.de
Fri Sep 26 15:59:50 CEST 2008


On Fri, 2008-09-26 at 04:25 +0200, Alexander Krauss wrote:
> So the only realistic chance is that users keep up with the development
> and update their theories.

Two (not necessarily great, as there is a tradeoff) ideas to assist with
that:

- Isabelle version headers in theory files (e.g., "Developed for
  Isabelle 2009"), possibly with Isabelle issuing a warning if
  missing/outdated.

- More tool/script support for automatic updating of theories.  (Similar
  to "isatool fixheaders", etc.  From an end-user's perspective, an
  automatic tool that could simply update current theory files to work
  with the next Isabelle version would probably be ideal.  Of course
  such a tool might be too difficult to develop though.)

Best,
Tjark




More information about the isabelle-dev mailing list