This sounds great! You seem to have done everything right. Having the compatibility mode will make it easy to get everything working again quickly, with the conversion to the new setup becoming a background task (possibly to be combined with refactoring horrible old proofs).
Larry On 14 Jan 2014, at 13:43, Thomas Sewell <thomas.sew...@nicta.com.au> wrote: > For those reasons I'd prefer to plough ahead as long as the impact is > manageable. I'll test the AFP and ISABELLE_FULL_TEST soon. I'm running out of > energy for this side project, however. If there is some collection of proofs > that are especially bad, we can just declare [[ hypsubst_thin = true ]] > globally in them, but I hope to avoid that for the same reason as (2) above: > having invisible adjustments to standard tactics seems like something we > should avoid. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
