Re: [isabelle] Transfer Isabelle2011 Code to Isabelle2014



Have you tried doing this port yet, so that you can report specific things that have been causing you problems? I can imagine many proofs that would go through unaltered.

There are no scripts for porting from one version to another.

I find it useful to run both the old and the new copies of Isabelle during porting. Then you can see where a proof goes wrong. Then the simplest thing is to see whether sledgehammer (greatly improved since 2011) can solve the problematical case.

Try to rewrite some of your proofs in the structured style. That gives you control over variable names and makes future porting much easier.

Larry Paulson


> On 13 Feb 2015, at 14:56, Sven Schneider <sven.schneider.pub at gmx.de> wrote:
> 
> Dear experts,
> 
> are there best practices to transfer Isabelle2011 (apply-style) code to
> Isabelle2014?
> For example, a shell-script to execute?
> What should be done before the transfer?
> 
> The AFP submission guidelines seem to imply that back and isabelle
> generated variable names are a source of backwards incompatibilty.
> Furthermore, I have encountered renamed/removed lemmas.
> 
> Is there a standard way to remove back? (I guess this is mostly the
> cases where the *allE* is used in my proofs; so I can image that the
> best way is to explicitly instantiate the P-variable.)
> 
> Is there a standard way to remove cases where Isabelle choses variable
> names? (I could explicitly set the names using rename_tac in all the
> places, but how do I detect such places?)
> 
> -- Sven Schneider
> <0xF0E2AE90.asc>





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