Re: [isabelle] Cancellation simprocs



And preferably, take the opportunity to clean up untidy proofs that are difficult to maintain. 
Larry

> 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
> proofs.
> * 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 MHonArc.