[isabelle] Transfer Isabelle2011 Code to Isabelle2014

Dear experts,

are there best practices to transfer Isabelle2011 (apply-style) code to
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

Attachment: 0xF0E2AE90.asc
Description: application/pgp-keys

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