We need to figure out how recdef does it. The minimum number of equations is mathematically fixed, so recdef must be using conditional expressions or other tricks. Larry
> On 9 Jun 2015, at 23:07, Gerwin Klein <gerwin.kl...@nicta.com.au> wrote: > > I can confirm that, at least that side is simple. > > Tobias’ point about avoiding exponential blowup is important, though. Might > still be too early to retire recdef entirely if it is substantially better > for some kinds of definitions, esp if they are in use (I think the recdef in > Simpl is one of these). > > Cheers, > Gerwin > >> On 09.06.2015, at 11:27, Thomas Sewell <thomas.sew...@nicta.com.au> wrote: >> >> I've had a quick scan over the NICTA repositories. It doesn't look like >> there are any live original uses of recdef. There are recdefs in a copy >> of Simpl-AFP, and in some backups of historical papers. >> >> Short summary, NICTA doesn't have any stakes in recdef. >> >> Cheers, >> Thomas. >> >> On 08/06/15 06:13, Makarius wrote: >>> On Sat, 6 Jun 2015, Gerwin Klein wrote: >>> >>>> >>>>> On 06.06.2015, at 21:23, Makarius <makar...@sketis.net> wrote: >>>>> >>>>> (2) 'defer_recdef' which is unused in the directly visible Isabelle >>>>> universe. So it could be deleted today. >>>>> >>>>> This mailing list thread is an opportunity to point out dark matter >>>>> in the Isabelle universe, where 'defer_recdef' still occurs. >>>>> Otherwise I will remove it soon, lets say within 1-2 weeks. >>>> >>>> Unused in our part of the dark matter universe as well. >>> >>> The thread has shifted over to actual 'recdef'. Are there remaining >>> uses of 'recdef' in the NICTA dark matter? >>> >>> So far I always thought the remaining uses in HOL-Decision_Procs are >>> only a reminder that there are other important applications. >>> >>> >>> Makarius > > > ________________________________ > > The information in this e-mail may be confidential and subject to legal > professional privilege and/or copyright. National ICT Australia Limited > accepts no liability for any damage caused by this email or its attachments. > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
