Re: [isabelle] Incompatibilities between releases (Re: Syntax for theory definitions)
On Fri, 26 Sep 2008, Burkhart Wolff wrote:
> I'd like to add, however, that the portability of CODE on the ML level
> is not that bad; Proofs break more often as tactic code in my
> experience. I am porting stuff since Isabelle 94 ...
This is also my experience. Even though ML interfaces often change
substantially, it is usually reasonable easy to port old code (thanks to
static type-checking in ML).
Proofs are much more fragile, notably unstructured ones. One way around
this is to submit theory libraries and applications to
http://afp.sourceforge.net/ where they get updated to latest Isabelle
This archive was generated by a fusion of
Pipermail (Mailman edition) and