Re: [isabelle] Transfer Isabelle2011 Code to Isabelle2014



Some lemmas from the standard library (HOL) have also been renamed. This
is usually documented in the NEWS-file ... if a lemma is missing, search
for its name in the NEWS-file, and you may find its new name ...

-- 
  Peter


On Sa, 2015-02-14 at 12:48 +0000, Larry Paulson wrote:
> 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.