Re: [isabelle] Cancellation simprocs
And preferably, take the opportunity to clean up untidy proofs that are difficult to maintain.
> On 4 Mar 2017, at 09:01, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> * Make the intended change.
> * See whether HOL can get run with reasonable effort.
> * Build as much as possible from distro and AFP. Iterate over breaking
> * Over time you get an idea what the impact of the change is:
> * How many breaking proofs?
> * How big is the amount of ÂawkwardÂ breaking proofs compared to
> ÂstreamlinedÂ breaking proofs?
> * Is there are recurring pattern how proofs can be repaired?
> * Is there yet another thing to change e.g. concerning the simplifier
> setup to get to a cleaner situation again?
This archive was generated by a fusion of
Pipermail (Mailman edition) and