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 
automagically.


	Makarius






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.